Abstract proof checking: An example motivated by an incompleteness theorem. (English) Zbl 0890.03004

This paper presents an example of proof checking with abstraction in the interactive proof checker GETFOL. Abstraction means that the user translates the original theory (and the conjecture) into an “abstract theory”. The user inputs the original theory and the abstract theory in GETFOL, as two separate contexts. Then, the user builds interactively with GETFOL a proof of the theorem in the abstract theory. Typically the user decides the instantiations of quantifiers, whereas the system provides decision procedures (e.g., a tautology checker for propositional logic). Then the abstract proof needs to be translated into a proof in the original theory. Since the abstraction does not have to preserve the semantics, there is no guarantee that the translation yields a proof in the original theory. GETFOL can generate from the abstract proof an outline of the proof in the original theory, and then the user has to complete it (e.g., by instantiating quantifiers) and check it interactively.


03B35 Mechanization of proofs and logical operations
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
Full Text: DOI