Automated Deduction - CADE-17: 17th International Conference on Automated Deduction Pittsburgh, PA, USA, June 17-20, 2000. Proceedings

Front Matter....Pages -
High-Level Verification Using Theorem Proving and Formalized Mathematics....Pages 1-6
Machine Instruction Syntax and Semantics in Higher Order Logic....Pages 7-24
Proof Generation in the Touchstone Theorem Prover....Pages 25-44
Wellfounded Schematic Definitions....Pages 45-63
Abstract Congruence Closure and Specializations....Pages 64-78
A Framework for Cooperating Decision Procedures....Pages 79-98
Modular Reasoning in Isabelle....Pages 99-114
An Infrastructure for Intertheory Reasoning....Pages 115-131
Gödel’s Algorithm for Class Formation....Pages 132-147
Automated Proof Construction in Type Theory Using Resolution....Pages 148-163
System Description: TPS: A Theorem Proving System for Type Theory....Pages 164-169
The Nuprl Open Logical Environment....Pages 170-176
System Description: aRa – An Automatic Theorem Prover for Relation Algebras....Pages 177-182
Scalable Knowledge Representation and Reasoning Systems....Pages 183-183
Efficient Minimal Model Generation Using Branching Lemmas....Pages 184-199
FDPLL — A First-Order Davis-Putnam-Logeman-Loveland Procedure....Pages 200-219
Rigid E -Unification Revisited....Pages 220-234
Connecting Bits with Floating-Point Numbers: Model Checking and Theorem Proving in Practice....Pages 235-235
Reducing Model Checking of the Many to the Few....Pages 236-254
Simulation Based Minimization....Pages 255-270
Rewriting for Cryptographic Protocol Verification....Pages 271-290
System Description: * sat : A Platform for the Development of Modal Decision Procedures....Pages 291-296
System Description: DLP....Pages 297-301
Two Techniques to Improve Finite Model Search....Pages 302-308
Eliminating Dummy Elimination....Pages 309-323
Extending Decision Procedures with Induction Schemes....Pages 324-345
Complete Monotonic Semantic Path Orderings....Pages 346-364
Stratified Resolution....Pages 365-384
Support Ordered Resolution....Pages 385-400
System Description: IVY....Pages 401-405
System Description: SystemOnTPTP ....Pages 406-410
System Description: PTTP+GLiDeS Semantically Guided PTTP....Pages 411-416
A Formalization of a Concurrent Object Calculus up to α -Conversion....Pages 417-432
A Resolution Decision Procedure for Fluted Logic....Pages 433-448
 ZRes : The Old Davis–Putnam Procedure Meets ZBDD....Pages 449-454
System Description: MBase , an Open Mathematical Knowledge Base....Pages 455-459
System Description: Tramp : Transformation of Machine-Found Proofs into Natural Deduction Proofs at the Assertion Level....Pages 460-464
On Unification for Bounded Distributive Lattices....Pages 465-481
Reasoning with Individuals for the Description Logic $\mathcal{SHIQ}$ ....Pages 482-496
System Description: Embedding Verification into Microsoft Excel....Pages 497-501
System Description: Interactive Proof Critics in XBarnacle....Pages 502-506
Tutorial: Meta-logical Frameworks....Pages 507-508
Tutorial: Automated Deduction and Natural Language Understanding....Pages 509-510
Tutorial: Using TPS for Higher-Order Theorem Proving and ETPS for Teaching Logic....Pages 511-512
Workshop: Model Computation – Principles, Algorithms, Applications....Pages 513-513
Workshop: Automation of Proof by Mathematical Induction....Pages 514-514
Workshop: Type-Theoretic Languages: Proof-Search and Semantics....Pages 515-515
Workshop: Automated Deduction in Education....Pages 516-516
Workshop: The Role of Automated Deduction in Mathematics....Pages 517-517
Back Matter....Pages -