Re: [isabelle] Deep embedding of natural deduction?


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


Dipl.-Math. Dipl.-Inform. Joachim Breitner
Wissenschaftlicher Mitarbeiter

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

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