Anzeige
Erschienen in:
2005 | OriginalPaper | Buchkapitel
Automatic ‘Descente Infinie’ Induction Reasoning
verfasst von : Sorin Stratulat
Erschienen in: Automated Reasoning with Analytic Tableaux and Related Methods
Verlag: Springer Berlin Heidelberg
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
We present a framework and a methodology to build and analyse automatic provers using the ’Descente Infinie’ induction principle. A stronger connection between different proof techniques like those based on implicit induction and saturation is established by uniformly and explicitly representing them as applications of this principle. The framework offers a clear separation between logic and computation, by the means of i) an abstract inference system that defines the maximal sets of induction hypotheses available at every step of a proof, and ii) reasoning modules that perform the computation and allow for modular design of the concrete inference rules. The methodology is applied to define a concrete implicit induction prover and analyse an existing saturation-based inference system.