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





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

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:

https://bitbucket.org/isafol/isafol/

We have just added a new entry that may be of interest:

Proof Systems for Propositional Logic

Tobias

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

http://www.collegepublications.co.uk/journals/ifcolog/

Regards,

Jørgen




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



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