Automated Theorem Proving

Monty Newborn ()
Additional contact information
Monty Newborn: McGill University, School of Computer Science

in Springer Books from Springer

Date: 2001
ISBN: 978-1-4613-0089-2
References: Add references at CitEc
Citations:

There are no downloads for this item, see the EconPapers FAQ for hints about obtaining it.

Chapters in this book:

Ch 1 A Brief Introduction to Compile, Herby, and Theo

Monty Newborn

Ch 2 Predicate Calculus, Well-Formed Formulas, and Theorems

Monty Newborn

Ch 3 Compile: Transforming Well-Formed Formulas to Clauses

Monty Newborn

Ch 4 Inference Procedures

Monty Newborn

Ch 5 Proving Theorems by Constructing Closed Semantic Trees

Monty Newborn

Ch 6 Resolution-Refutation Proofs

Monty Newborn

Ch 7 Herby: A Semantic—Tree Theorem Prover

Monty Newborn

Ch 8 Using Herby

Monty Newborn

Ch 9 Theo:A Resolution—Refutation Theorem Prover

Monty Newborn

Ch 10 Using Theo

Monty Newborn

Ch 11 A Look at the Source Code of Herby

Monty Newborn

Ch 12 A Look at the Source Code of Theo

Monty Newborn

Ch 13 The Cade Atp System Competitions and Other Theorem Provers

Monty Newborn

Related works:
This item may be available elsewhere in EconPapers: Search for items with the same title.

Export reference: BibTeX RIS (EndNote, ProCite, RefMan) HTML/Text

Persistent link: https://EconPapers.repec.org/RePEc:spr:sprbok:978-1-4613-0089-2

Ordering information: This item can be ordered from
http://www.springer.com/9781461300892

DOI: 10.1007/978-1-4613-0089-2

Access Statistics for this book

More books in Springer Books from Springer
Bibliographic data for series maintained by Sonal Shukla () and Springer Nature Abstracting and Indexing ().