Email Gateway (Aug 22 2022 at 15:07): Email Gateway (Aug 22 2022 at 15:07):From: Jørgen Villadsen <jovi@dtu.dk>
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 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
Email Gateway (Aug 22 2022 at 15:08):From: Tobias Nipkow <nipkow@in.tum.de>
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:
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 2017http://www.collegepublications.co.uk/journals/ifcolog/
Regards,
Jørgen
Email Gateway (Aug 22 2022 at 15:09):From: Jørgen Villadsen <jovi@dtu.dk>
Thank you very much for pointing out the impressive new work.
Jørgen
-----Original Message-----
From: cl-isabelle-users-bounces@lists.cam.ac.uk [mailto:cl-isabelle-users-bounces@lists.cam.ac.uk] On Behalf Of Tobias Nipkow
Sent: 24. februar 2017 12:06
To: cl-isabelle-users@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:
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 2017http://www.collegepublications.co.uk/journals/ifcolog/
Regards,
Jørgen
Last updated: Apr 24 2024 at 01:07 UTC