[isabelle] Formalization of soundness and completeness of natural deduction


My student Andreas Halkjær From is going to make nice Isar proofs of Stefan Berghofer's FOL-Fitting entry in the Archive for Formal Proofs for his bachelor project - are there any similar efforts?

Initially it will be an entry in the "Isabelle Formalization of Logic" repository:


We are aware of the following related entries:

https://www.isa-afp.org/entries/Incredible_Proof_Machine.shtml (Joachim Breitner and Denis Lohner)
https://www.isa-afp.org/entries/Abstract_Completeness.shtml (Jasmin Christian Blanchette, Andrei Popescu and Dmitriy Traytel)
https://www.isa-afp.org/entries/Verified-Prover.shtml (Tom Ridge)

In our recent paper we have very detailed Isar proofs but only of soundness:

NaDeA: A Natural Deduction Assistant with a Formalization in Isabelle
Jørgen Villadsen, Alexander Birch Jensen & Anders Schlichtkrull
IFCoLog Journal of Logics and their Applications 4(1) p. 55-82 2017




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.