Re: [isabelle] Formalization of soundness and completeness of natural deduction

On 23/02/2017 00:05, Jørgen Villadsen wrote:

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 have just added a new entry that may be of interest:

Proof Systems for Propositional Logic


We are aware of the following related entries: (Joachim Breitner and Denis Lohner) (Jasmin Christian Blanchette, Andrei Popescu and Dmitriy Traytel) (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



Attachment: smime.p7s
Description: S/MIME Cryptographic Signature

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