Re: [isabelle] Deep embedding of natural deduction?



Hi,

thanks for the overview, especially for the comments!

Am Donnerstag, den 07.01.2016, 11:02 +0100 schrieb Dmitriy Traytel:
> 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.

good guess :-)

I want to show that proof graphs, as they are used by the Incredible
Proof Machines, correspond to ânormalâ natural deduction trees, by
giving a mapping from proof blocks to inference rules and from graphs
to derivation trees, and at least show soundness, preferably also
completeness.

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.