2005 | OriginalPaper | Buchkapitel
History and Future of Implicit and Inductionless Induction: Beware the Old Jade and the Zombie!
verfasst von : Claus-Peter Wirth
Erschienen in: Mechanizing Mathematical Reasoning
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
In this survey on implicit induction I recollect some memories on the history of implicit induction as it is relevant for future research on computer-assisted theorem proving, esp. memories that significantly differ from the presentation in a recent handbook article on “inductionless induction”. Moreover, the important references excluded there are provided here. In order to clear the fog a little, there is a short introduction to inductive theorem proving and a discussion of connotations of implicit induction like “
descente infinie
”, “inductionless induction”, “proof by consistency”, implicit induction orderings (term orderings), and refutational completeness.