![](https://dblp.dagstuhl.de/img/logo.ua.320x120.png)
![](https://dblp.dagstuhl.de/img/dropdown.dark.16x16.png)
![](https://dblp.dagstuhl.de/img/peace.dark.16x16.png)
Остановите войну!
for scientists:
![search dblp search dblp](https://dblp.dagstuhl.de/img/search.dark.16x16.png)
![search dblp](https://dblp.dagstuhl.de/img/search.dark.16x16.png)
default search action
17th 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
![](https://dblp.dagstuhl.de/img/cog.dark.24x24.png)
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.