Skip to main content

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

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

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.

Metadaten
Titel
The AFFIRM theorem prover: Proof forests and management of large proofs
verfasst von
Roddy W. Erickson
David R. Musser
Copyright-Jahr
1980
Verlag
Springer Berlin Heidelberg
DOI
https://doi.org/10.1007/3-540-10009-1_18

Premium Partner