CODEWITHSUNDEEP
isabelle
g_d
g_d

Reputation: 707

Classical proof extraction in Isabelle. Do terms exist in somewhere in memory?

I found similar question here: (5-year old, no answer) https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2014-October/msg00120.html , but it is not the same.

Let's assume I've proved classical theorem like "((A->B)/\((~A)->B))->B". Is it possible in Isabelle to extract the term similar to one from page 10 of this paper: http://www21.in.tum.de/~berghofe/papers/TYPES2002_slides.pdf .

I think this is important to make proofs framework-independent. But I also suspect that they may not be obtained because they do not exist! For example, there is a decision procedures, which may decide whether propositional formula is a tautology. But no explicit term is generated during this procedure. Are proofs in Isabelle "honest" or "fast" in this sense? (I am particularly interested in Isabelle/ZF)

Upvotes: 1

Views: 115

Answers (1)

Alex Krauss
Alex Krauss

Reputation: 10393

Isabelle reduces all proofs to primitive inferences, but does not record explicit proof terms by default unless you explicitly ask for it (which also leads to a noticable performance hit). Even when proof recording is off, inferences are checked by the kernel, which reduces them to primitive inferences. This also includes decision procedures which are typically proof producing, although it is also possible to integrate decision procedures as unsafe oracles. In this sense, Isabelle is "honest", using your terminology above.

Full proof terms can be printed and accessed via some ML programming, but tools for export are not well-developed (as of 2019), since most users do not care so much about the proof terms.

Upvotes: 2

Related Questions