Commit ee1fe9d4 authored by Ulrich's avatar Ulrich

the project builds again + minor textual changes

parent c0e4dfe9
......@@ -695,8 +695,8 @@ Hint Resolve eq_sym eq_trans eq_congr_or eq_dneg or_dneg : eq_orDB.
Lemma axiom_id:
forall Z G, KIbox Z G Z.
Proof.
intros.
replace Z with (sub sub_id Z) at 2 by apply sub_id_ok.
intros Z G.
rewrite <- sub_id_ok at 2.
apply KIbox_axiom.
Qed.
......
......@@ -28,14 +28,14 @@ This file does not contain any coq code. It is an overview of the dnegmod projec
The formalization contains a couple of hint databases, which are briefly explained here.
- [KIboxDB]: This database includes the constructors of the natural
deduction system for the intuitionistic modal logic, weakening, not_intro
and not_elim (compare the part about negations). It is widely used throughout
deduction system for the intuitionistic modal logic, [weakening], [not_intro]
and [not_elim] (compare the part about negations). It is widely used throughout
this work mostly with a limiting number of steps (often 3, sometimes 4).
- [eq_impDB, eq_andDB, eq_orDB]: These three all contain the fact that
equality is symmetric, transitive and monotonic by double negation.
Additionally, they also include important double negation theorem
Additionally, they also include important double negation theorems
from Oliva & Ferreira ([[DNEG]]) and congruence for implication,
conjunction and disjunction respectively. Using these
databases, we could shorten proofs involving only simple
......@@ -90,5 +90,7 @@ This section provides an overview of the tactics defined throughout the project.
-[[RUI]] Tadeusz Litak's formalization of W. Ruitenburg JSL 1984 paper "On the Period of Sequences (An(p)) in Intuitionistic Propositional Calculus"
-[[CMP]] Litak, Tadeusz. "Constructive modalities with provability smack." Leo Esakia on Duality in Modal and Intuitionistic Logics. Springer Netherlands, 2014. 187-216.
-[[CML]] Bellin, Gianluigi, Valeria De Paiva, and Eike Ritter. "Extended Curry-Howard correspondence for a basic constructive modal logic." In Proceedings of Methods for Modalities. 2001.
-[[DNM]] Litak, Tadeusz. "Double Negation and Modality" ALCOP 2016. File "alcop2016slides_corrected_extended.pdf" in the projects repository.
-[[DNM]] Litak, Tadeusz. "Double Negation and Modality" ALCOP 2016.
File "alcop2016slides_corrected_extended.pdf" in the projects repository.
*)
\ No newline at end of file
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment