Modal logic

Content created by Viktor Yudov.

Created on 2023-10-23.
Last modified on 2024-05-31.

module modal-logic where

open import modal-logic.axioms public
open import modal-logic.canonical-model-theorem public
open import modal-logic.canonical-theories public
open import modal-logic.closed-under-subformulas-theories public
open import modal-logic.completeness public
open import modal-logic.completeness-k public
open import modal-logic.completeness-s5 public
open import modal-logic.decision-procedure public
open import modal-logic.deduction public
open import modal-logic.filtrated-kripke-classes public
open import modal-logic.filtration-lemma public
open import modal-logic.finite-approximability public
open import modal-logic.formulas public
open import modal-logic.formulas-deduction public
open import modal-logic.kripke-models-filtrations public
open import modal-logic.kripke-semantics public
open import modal-logic.l-complete-theories public
open import modal-logic.l-consistent-theories public
open import modal-logic.lindenbaum public
open import modal-logic.minimal-kripke-filtration public
open import modal-logic.minimal-transitive-kripke-filtration public
open import modal-logic.modal-logic-k public
open import modal-logic.modal-logic-s5 public
open import modal-logic.soundness public
open import modal-logic.subformulas public
open import modal-logic.weak-deduction public

Recent changes