Search from the table of contents of 2.5 million books
Advanced Search (Beta)
Home > Automated Deduction - CADE-17: 17th International Conference on Automated Deduction Pittsburgh, PA, USA, June 17-20, 2000 Proceedings > System Description: Interactive Proof Critics in XBarnacle
Automated Deduction - CADE-17: 17th International Conference on Automated Deduction Pittsburgh, PA, USA, June 17-20, 2000 Proceedings |
David McAllester
Springer Berlin Heidelberg
Automated Deduction - CADE-17: 17th International Conference on Automated Deduction Pittsburgh, PA, USA, June 17-20, 2000 Proceedings
System Description: Interactive Proof Critics in XBarnacle
Authors

Mike Jackson; Helen Lowe

ARI Id

1664702458940_2805169

Access

Not Available Free

Pages

502-506

DOI

10.1007/10721959_41

Chapter URL

https://rd.springer.com/chapter/10.1007/10721959_41

Table of Contents of Book
Showing 1 to 20 of 51 entries
Chapters/HeadingsAuthor(s)PagesInfo
Front Matter
High-Level Verification Using Theorem Proving and Formalized Mathematics
John Harrison
1-6
Machine Instruction Syntax and Semantics in Higher Order Logic
Neophytos G. Michael; Andrew W. Appel
7-24
Proof Generation in the Touchstone Theorem Prover
George C. Necula; Peter Lee
25-44
Wellfounded Schematic Definitions
Konrad Slind
45-63
Abstract Congruence Closure and Specializations
Leo Bachmair; Ashish Tiwari
64-78
A Framework for Cooperating Decision Procedures
Clark W. Barrett; David L. Dill; Aaron Stump
79-98
Modular Reasoning in Isabelle
Florian Kammüller
99-114
An Infrastructure for Intertheory Reasoning
William M. Farmer
115-131
Gödel’s Algorithm for Class Formation
Johan Gijsbertus Frederik Belinfante
132-147
Automated Proof Construction in Type Theory Using Resolution
Marc Bezem; Dimitri Hendriks; Hans de Nivelle
148-163
System Description: TPS: A Theorem Proving System for Type Theory
Peter B. Andrews; Matthew Bishop; Chad E. Brown
164-169
The Nuprl Open Logical Environment
Stuart F. Allen; Robert L. Constable; Rich Eaton; Christoph Kreitz; Lori Lorigo
170-176
System Description: aRa – An Automatic Theorem Prover for Relation Algebras
Carsten Sinz
177-182
Scalable Knowledge Representation and Reasoning Systems
Henry Kautz
183-183
Efficient Minimal Model Generation Using Branching Lemmas
Ryuzo Hasegawa; Hiroshi Fujita; Miyuki Koshimura
184-199
FDPLL — A First-Order Davis-Putnam-Logeman-Loveland Procedure
Peter Baumgartner
200-219
Rigid E-Unification Revisited
Ashish Tiwari; Leo Bachmair; Harald Ruess
220-234
Connecting Bits with Floating-Point Numbers: Model Checking and Theorem Proving in Practice
Carl-Johan Seger
235-235
Reducing Model Checking of the Many to the Few
E. Allen Emerson; Vineet Kahlon
236-254
Chapters/HeadingsAuthor(s)PagesInfo
Showing 1 to 20 of 51 entries
Similar Books
Similar Chapters
Similar Thesis

Similar News

Similar Articles
Similar Article Headings