Re: [isabelle] Deep embedding of natural deduction?



Hi Joachim,

here are some related references (none of which has all you need):

1. Margetson, Ridge: http://afp.sourceforge.net/entries/Completeness.shtml <http://afp.sourceforge.net/entries/Completeness.shtml> (see also the TPHOLs 2005 paper http://dx.doi.org/10.1007/11541868_19)

Similar to JÃrgen Villadsenâs theory it hard-codes formulas and natural deduction inference rules. It has a notion of valid trees and used de Bruijn indices for variables. The entry proves soundness and completeness of FOL.

2. Berghofer: http://afp.sourceforge.net/entries/FOL-Fitting.shtml <http://afp.sourceforge.net/entries/FOL-Fitting.shtml>

Another formalization of FOL soundness and completeness (+LÃwenheim-Skolem) for a natural deduction calculus. No derivation trees though (Stefan follows a semantic approach, which does not require them).

3. Blanchette, Popescu, Traytel: http://afp.sourceforge.net/entries/Abstract_Completeness.shtml <http://afp.sourceforge.net/entries/Abstract_Completeness.shtml> (see also the IJCARâ14 paper http://dx.doi.org/10.1007/978-3-319-08587-6_4 <http://dx.doi.org/10.1007/978-3-319-08587-6_4> or its extended draft article http://people.inf.ethz.ch/trayteld/papers/fol_completeness2/compl2.pdf)

This one has abstract (syntax-independent) notions of valid proof trees. It aims at formulating the completeness property as abstractly as possible. (The journal version also shows abstract soundness for classic FOL and extensions; the archive attachment  
http://people.inf.ethz.ch/trayteld/compl-journal-devel.tgz <http://people.inf.ethz.ch/trayteld/compl-journal-devel.tgz> contains the formalizations of these extensions). In the AFP there is only a toy instantiation of the abstract machinery with propositional logic.

There is also a sophisticated instantiation with many-sorted FOL by and a natural deduction proof system Andrei and Jasmin (for their Mechanization of Sledgehammerâs metatheory) that uses Andreiâs theory of Syntax with Bindings. All of this is not in the AFP but available separately, http://www21.in.tum.de/~traytel/compl_devel.zip <http://www21.in.tum.de/~traytel/compl_devel.zip>, tested with Isabelle2013-2 ;-) ; see readme.txt there.

4. Sternagel, Thiemann, et al.: IsaFoR (http://cl-informatik.uibk.ac.at/software/ceta/index.php <http://cl-informatik.uibk.ac.at/software/ceta/index.php>)

It has the most developed formalization of first-order terms (including matching, unification, and what not).

5. Blanchette, Fleury, Schlichtkrull, Traytel: IsaFoL (https://bitbucket.org/jasmin_blanchette/isafol)

Formalizes logical calculi (ongoing work, so far with a focus on resolution and superposition, not so much on natural deduction).

Iâm not sure what your precise application is (formalization of the incredible proof machine?, what do you want to prove there?). If you aim for soundness and completeness, building on top of 3 and 4 might be a way to go.

Hope that helps,
Dmitriy

> On 05 Jan 2016, at 13:46, Joachim Breitner <breitner at kit.edu> wrote:
> 
> Dear List,
> 
> Iâm searching for a formal description of natural deduction, preferably
> formalized in Isabelle.
> 
> What I found was for example this theory
> https://github.com/logic-tools/nadea/blob/master/Isabelle/NaDeA.thy
> (part of https://nadea.compute.dtu.dk/ by JÃrgen Villadsen)
> but it hard-codes the terms and inference rules; Iâm interested in 
> something more general, where the terms (or at least the connectives)
> are abstract, and also the set of inference rules is not fixed.
> 
> In other words: Iâm looking for a data type that can describe arbitrary
> terms (with binders), inference rules and derivation tree using them,
> and can determine whether the derivation tree is valid (terms match,
> only the given inference rules are used, scoping of variables is
> correct).
> 
> Do you know of such a thing?
> 
> Greetings,
> Joachim
> 
> 
> -- 
> Dipl.-Math. Dipl.-Inform. Joachim Breitner
> Wissenschaftlicher Mitarbeiter
> http://pp.ipd.kit.edu/~breitner
> 




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