1980 | ReviewPaper | Buchkapitel
The AFFIRM theorem prover: Proof forests and management of large proofs
verfasst von : Roddy W. Erickson, David R. Musser
Erschienen in: 5th Conference on Automated Deduction Les Arcs, France, July 8–11, 1980
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
The AFFIRM theorem prover is an interative, natural-deduction system centered around abstract data types. Since long proofs are often required to verity algorithms, we describe a model (called the "proof forest") which helps the user to visualize and manage the potentially large number of theorems and subgoals that can arise.