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



Thank you very much for pointing out the impressive new work.

Jørgen

-----Original Message-----
From: cl-isabelle-users-bounces at lists.cam.ac.uk [mailto:cl-isabelle-users-bounces at lists.cam.ac.uk] On Behalf Of Tobias Nipkow
Sent: 24. februar 2017 12:06
To: cl-isabelle-users at lists.cam.ac.uk
Subject: 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
>
>
>





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