2002 | OriginalPaper | Buchkapitel
Proof Analysis by Resolution
Abstract
verfasst von : Matthias Baaz
Erschienen in: Automated Reasoning with Analytic Tableaux and Related Methods
Verlag: Springer Berlin Heidelberg
Enthalten in: Professional Book Archive
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
Proof analysis of existing proofs is one of the main sources of scientific progress in mathematics: new concepts can be obtained, e.g., by denoting explicit definitions in proof parts and axiomatizing them as new mathematical objects in their own right. (The development of the concept of integral is a well known example.) All forms of proof analysis are intended to make implicit information of a proof explicit, i.e., visible. Logical proof analysis is mainly concerned with the implicit constructive content of more or less formalized proofs.The following are major examples for logical proof analysis: Formal proofs of (∀x)(∃y)P(x, y) in computational contexts can be unwinded to proofs of (∀x)P(x,π(x)) for suitable programs π.Herbrand disjunctions can be extracted from proofs of prenex formulas. Such disjunctions always exist in the case of first-order logic by Herbrand’s famous theorem, but can be extracted from many proofs in other systems as well. (C.f. Luckhardt’s analysis of the proof of Roth’s theorem.) Suitable Herbrand disjunctions can be used to improve bounds or to reduce parametrical dependencies.Interpolants can be constructed from proofs of A → B. Interpolation is the main tool to make implicit definitions explicit via Beth’s theorem.