Automated deduction – CADE-17 : 17th International Conference on Automated Deduction, Pittsburgh, PA, USA, June 17-20, 2000 : proceedings

Automated Deduction - CADE-17: 17th International Conference on Automated Deduction Pittsburgh, PA, USA, June 17-20, 2000. Proceedings
Author: David McAllester
Published by Springer Berlin Heidelberg
ISBN: 978-3-540-67664-5
DOI: 10.1007/10721959

Table of Contents:

• High-Level Verification Using Theorem Proving and Formalized Mathematics
• Machine Instruction Syntax and Semantics in Higher Order Logic
• Proof Generation in the Touchstone Theorem Prover
• Wellfounded Schematic Definitions
• Abstract Congruence Closure and Specializations
• A Framework for Cooperating Decision Procedures
• Modular Reasoning in Isabelle
• An Infrastructure for Intertheory Reasoning
• Gödel’s Algorithm for Class Formation
• Automated Proof Construction in Type Theory Using Resolution
• System Description: TPS: A Theorem Proving System for Type Theory
• The Nuprl Open Logical Environment
• System Description: aRa – An Automatic Theorem Prover for Relation Algebras
• Scalable Knowledge Representation and Reasoning Systems
• Efficient Minimal Model Generation Using Branching Lemmas
• FDPLL — A First-Order Davis-Putnam-Logeman-Loveland Procedure
• Rigid E-Unification Revisited
• Connecting Bits with Floating-Point Numbers: Model Checking and Theorem Proving in Practice
• Reducing Model Checking of the Many to the Few
• Simulation Based Minimization

Includes bibliographical references and index