Abstract is missing.
- High-Level Verification Using Theorem Proving and Formalized MathematicsJohn Harrison. 1-6
- Machine Instruction Syntax and Semantics in Higher Order LogicNeophytos G. Michael, Andrew W. Appel. 7-24
- Proof Generation in the Touchstone Theorem ProverGeorge C. Necula, Peter Lee. 25-44
- Wellfounded Schematic DefinitionsKonrad Slind. 45-63
- Abstract Congruence Closure and SpecializationsLeo Bachmair, Ashish Tiwari. 64-78
- A Framework for Cooperating Decision ProceduresClark W. Barrett, David L. Dill, Aaron Stump. 79-98
- Modular Reasoning in IsabelleFlorian Kammüller. 99-114
- An Infrastructure for Intertheory ReasoningWilliam M. Farmer. 115-131
- Gödel s Algorithm for Class FormationJohan G. F. Belinfante. 132-147
- Automated Proof Construction in Type Theory Using ResolutionMarc Bezem, Dimitri Hendriks, Hans de Nivelle. 148-163
- System Description: TPS: A Theorem Proving System for Type TheoryPeter B. Andrews, Matthew Bishop, Chad E. Brown. 164-169
- The Nuprl Open Logical EnvironmentStuart F. Allen, Robert L. Constable, Richard Eaton, Christoph Kreitz, Lori Lorigo. 170-176
- System Description: ARA - An Automatic Theorem Prover for Relation AlgebrasCarsten Sinz. 177-182
- Scalable Knowledge Representation and Reasoning SystemsHenry A. Kautz. 183
- Efficient Minimal Model Generation Using Branching LemmasRyuzo Hasegawa, Hiroshi Fujita, Miyuki Koshimura. 184-199
- FDPLL - A First Order Davis-Putnam-Longeman-Loveland ProcedurePeter Baumgartner. 200-219
- Rigid ::::E::::-Unification RevisitedAshish Tiwari, Leo Bachmair, Harald Rueß. 220-234
- Connecting Bits with Floating-Point Numbers: Model Checking and Theorem Proving in PracticeCarl-Johan H. Seger. 235
- Reducing Model Checking of the Many to the FewE. Allen Emerson, Vineet Kahlon. 236-254
- Simulation Based MinimizationDoron Bustan, Orna Grumberg. 255-270
- Rewriting for Cryptographic Protocol VerificationThomas Genet, Francis Klay. 271-290
- System Description: *SAT: A Platform for the Development of Modal Decision ProceduresEnrico Giunchiglia, Armando Tacchella. 291-296
- System Description: DLPPeter F. Patel-Schneider. 297-301
- Two Techniques to Improve Finite Model SearchGilles Audemard, Belaid Benhamou, Laurent Henocque. 302-308
- Eliminating Dummy EliminationJürgen Giesl, Aart Middeldorp. 309-323
- Extending Decision Procedures with Induction SchemesDeepak Kapur, Mahadevan Subramaniam. 324-345
- Complete Monotonic Semantic Path OrderingsCristina Borralleras, Maria Ferreira, Albert Rubio. 346-364
- Stratified ResolutionAnatoli Degtyarev, Andrei Voronkov. 365-384
- Support Ordered ResolutionBruce Spencer, Joseph Douglas Horton. 385-400
- System Description: IVYWilliam McCune, Olga Shumsky. 401-405
- System Description: SystemOn TPTPGeoff Sutcliffe. 406-410
- System Description: PTTP+GLiDes: Semantically Guided PTTPMarianne Brown, Geoff Sutcliffe. 411-416
- A Formalization of a Concurrent Object Calculus up to alpha-ConversionGuillaume Gillard. 417-432
- A Resolution Decision Procedure for Fluted LogicRenate A. Schmidt, Ullrich Hustadt. 433-448
- ZRES: The Old Davis-Putman Procedure Meets ZBDDPhilippe Chatalic, Laurent Simon. 449-454
- System Description: MBASE, an Open Mathematical Knowledge BaseAndreas Franke, Michael Kohlhase. 455-459
- System Description: TRAMP: Transformation of Machine-Found Proofs into ND-Proofs at the Assertion LevelAndreas Meier. 460-464
- On Unification for Bonded Distributive LatticesViorica Sofronie-Stokkermans. 465-481
- Reasoning with Individuals for the Description Logic SHIQIan Horrocks, Ulrike Sattler, Stephan Tobies. 482-496
- System Description: Embedding Verification into Microsoft ExcelGraham Collins, Louise A. Dennis. 497-501
- System Description: Interactive Proof Critics in XBarnacleMichael Jackson, Helen Lowe. 502-506
- Tutorial: Meta-logical FrameworksCarsten Schürmann. 507-508
- Tutorial: Automated Deduction and Natural Language UnderstandingStephen G. Pulman. 509-510
- Tutorial: Using TPS for Higher-Order Theorem Proving and ETPS for Teaching LogicPeter B. Andrews, Chad E. Brown. 511-512
- Workshop: Model Computation - Principles, Algorithms, ApplicationsPeter Baumgartner, Christian G. Fermüller, Nicolas Peltier, Hantao Zhang. 513
- Workshop: Automation of Proofs by Mathematical InductionCarsten Schürmann. 514
- Workshop: Type-Theoretic Languages: Proof-Search and SemanticsDidier Galmiche. 515
- Workshop: Automated Deduction in EducationErica Melis. 516
- Workshop: The Role of Automated Deduction in MathematicsSimon Colton, Volker Sorge, Ursula Martin. 517