[isabelle] Deep embedding of natural deduction?



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

Attachment: signature.asc
Description: This is a digitally signed message part



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