default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCID17th CADE 2000: Pittsburgh, PA, USA
- David A. McAllester:
Automated Deduction - CADE-17, 17th International Conference on Automated Deduction, Pittsburgh, PA, USA, June 17-20, 2000, Proceedings. Lecture Notes in Computer Science 1831, Springer 2000, ISBN 3-540-67664-3
Invited Talk
- John Harrison:
High-Level Verification Using Theorem Proving and Formalized Mathematics. 1-6
Session 1:
- Neophytos G. Michael, Andrew W. Appel:
Machine Instruction Syntax and Semantics in Higher Order Logic. 7-24 - George C. Necula, Peter Lee:
Proof Generation in the Touchstone Theorem Prover. 25-44 - Konrad Slind:
Wellfounded Schematic Definitions. 45-63
Session 2:
- Leo Bachmair, Ashish Tiwari:
Abstract Congruence Closure and Specializations. 64-78 - Clark W. Barrett, David L. Dill, Aaron Stump:
A Framework for Cooperating Decision Procedures. 79-98 - Florian Kammüller:
Modular Reasoning in Isabelle. 99-114 - William M. Farmer:
An Infrastructure for Intertheory Reasoning. 115-131
Session 3:
- Johan G. F. Belinfante:
Gödel's Algorithm for Class Formation. 132-147 - Marc Bezem, Dimitri Hendriks, Hans de Nivelle:
Automated Proof Construction in Type Theory Using Resolution. 148-163 - Peter B. Andrews, Matthew Bishop, Chad E. Brown:
System Description: TPS: A Theorem Proving System for Type Theory. 164-169 - Stuart F. Allen, Robert L. Constable, Richard Eaton, Christoph Kreitz, Lori Lorigo:
The Nuprl Open Logical Environment. 170-176 - Carsten Sinz:
System Description: ARA - An Automatic Theorem Prover for Relation Algebras. 177-182
Invited Talk
- Henry A. Kautz:
Scalable Knowledge Representation and Reasoning Systems. 183
Session 4:
- Ryuzo Hasegawa, Hiroshi Fujita, Miyuki Koshimura:
Efficient Minimal Model Generation Using Branching Lemmas. 184-199 - Peter Baumgartner:
FDPLL - A First Order Davis-Putnam-Longeman-Loveland Procedure. 200-219 - Ashish Tiwari, Leo Bachmair, Harald Rueß:
Rigid E-Unification Revisited. 220-234
Invited Talk
- Carl-Johan H. Seger:
Connecting Bits with Floating-Point Numbers: Model Checking and Theorem Proving in Practice. 235
Session 5:
- E. Allen Emerson, Vineet Kahlon:
Reducing Model Checking of the Many to the Few. 236-254 - Doron Bustan, Orna Grumberg:
Simulation Based Minimization. 255-270 - Thomas Genet, Francis Klay:
Rewriting for Cryptographic Protocol Verification. 271-290 - Enrico Giunchiglia
, Armando Tacchella:
System Description: *SAT: A Platform for the Development of Modal Decision Procedures. 291-296 - Peter F. Patel-Schneider:
System Description: DLP. 297-301 - Gilles Audemard, Belaid Benhamou, Laurent Henocque:
Two Techniques to Improve Finite Model Search. 302-308
Session 6:
- Jürgen Giesl, Aart Middeldorp:
Eliminating Dummy Elimination. 309-323 - Deepak Kapur, Mahadevan Subramaniam:
Extending Decision Procedures with Induction Schemes. 324-345 - Cristina Borralleras, Maria Ferreira, Albert Rubio:
Complete Monotonic Semantic Path Orderings. 346-364
Session 7:
- Anatoli Degtyarev, Andrei Voronkov:
Stratified Resolution. 365-384 - Bruce Spencer, Joseph Douglas Horton:
Support Ordered Resolution. 385-400 - William McCune, Olga Shumsky:
System Description: IVY. 401-405 - Geoff Sutcliffe:
System Description: SystemOn TPTP. 406-410 - Marianne Brown, Geoff Sutcliffe:
System Description: PTTP+GLiDes: Semantically Guided PTTP. 411-416
Session 8:
- Guillaume Gillard:
A Formalization of a Concurrent Object Calculus up to alpha-Conversion. 417-432 - Renate A. Schmidt, Ullrich Hustadt:
A Resolution Decision Procedure for Fluted Logic. 433-448 - Philippe Chatalic, Laurent Simon:
ZRES: The Old Davis-Putman Procedure Meets ZBDD. 449-454 - Andreas Franke, Michael Kohlhase:
System Description: MBASE, an Open Mathematical Knowledge Base. 455-459 - Andreas Meier:
System Description: TRAMP: Transformation of Machine-Found Proofs into ND-Proofs at the Assertion Level. 460-464
Session 9:
- Viorica Sofronie-Stokkermans:
On Unification for Bonded Distributive Lattices. 465-481 - Ian Horrocks, Ulrike Sattler, Stephan Tobies:
Reasoning with Individuals for the Description Logic SHIQ. 482-496 - Graham Collins, Louise A. Dennis:
System Description: Embedding Verification into Microsoft Excel. 497-501 - Mike Jackson, Helen Lowe:
System Description: Interactive Proof Critics in XBarnacle. 502-506
Tutorials
- Carsten Schürmann:
Tutorial: Meta-logical Frameworks. 507-508 - Stephen G. Pulman:
Tutorial: Automated Deduction and Natural Language Understanding. 509-510 - Peter B. Andrews, Chad E. Brown:
Tutorial: Using TPS for Higher-Order Theorem Proving and ETPS for Teaching Logic. 511-512
Workshops
- Peter Baumgartner, Christian G. Fermüller, Nicolas Peltier, Hantao Zhang:
Workshop: Model Computation - Principles, Algorithms, Applications. 513 - Carsten Schürmann:
Workshop: Automation of Proofs by Mathematical Induction. 514 - Didier Galmiche:
Workshop: Type-Theoretic Languages: Proof-Search and Semantics. 515 - Erica Melis:
Workshop: Automated Deduction in Education. 516 - Simon Colton, Volker Sorge, Ursula Martin:
Workshop: The Role of Automated Deduction in Mathematics. 517
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
last updated on 2025-03-01 15:01 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
