Abstract is missing.
- The Crisis in Finite Mathematics: Automated Reasoning as Cause and CureJohn K. Slaney. 1-13
- A Divergence CriticToby Walsh. 14-28
- Synthesis of Induction Orderings for Existence ProofsDieter Hutter. 29-41
- Lazy Generation of Induction HypothesesMartin Protzen. 42-56
- The Search Efficiency of Theorem Proving StrategiesDavid A. Plaisted. 57-71
- A Method for Building Models Automatically. Experiments with an Extension of OTTERChristophe Bourely, Ricardo Caferra, Nicolas Peltier. 72-86
- Model Elimination Without ContrapositivesPeter Baumgartner, Ulrich Furbach. 87-101
- Induction using Term OrderingsFrançois Bronsard, Uday S. Reddy, Robert W. Hasker. 102-117
- Mechanizable Inductive Proofs for a Class of Forall Exists FormulasJacques Chazarain, Emmanuel Kounalis. 118-132
- On the Connection between Narrowing and Proof by ConsistencyOlav Lysne. 133-147
- A Fixedpoint Approach to Implementing (Co)Inductive DefinitionsLawrence C. Paulson. 148-161
- On Notions of Inductive Validity for First-Oder Equational ClausesClaus-Peter Wirth, Bernhard Gramlich. 162-176
- A New Application for Explanation-Based Generalisation within Automated DeductionSiani Baker. 177-191
- Semantically Guided First-Order Theorem Proving using Hyper-LinkingHeng Chu, David A. Plaisted. 192-206
- The Applicability of Logic Program Analysis and Transformation to Theorem ProvingD. Andre de Waal, John P. Gallagher. 207-221
- Detecting Non-Provable GoalsStefan Brüning. 222-236
- Panel Discussion: A Mechanically Proof-Checked Encyclopedia of Mathematics: Should We Build One? Can We?Robert S. Boyer. 237
- The QED Manifesto238-251
- The TPTP Problem LibraryGeoff Sutcliffe, Christian B. Suttner, Theodor Yemenis. 252-266
- Combination Techniques for Non-Disjoint Equational TheoriesEric Domenjoud, Francis Klay, Christophe Ringeissen. 267-281
- Primal Grammars and Unification Modulo a Binary ClauseGernot Salzer. 282-295
- Conservative Query Normalization on Parallel CircumscriptionKoji Iwanuma. 296-310
- Bottom-up Evaluation of Datalog Programs with Arithmetic ConstraintsLaurent Fribourg, Marcos Veloso Peixoto. 311-325
- On Intuitionistic Query Answering in Description BasesVéronique Royer, Joachim Quantz. 326-340
- Deductive Composition of Astronomical Software from Subroutine LibrariesMark E. Stickel, Richard J. Waldinger, Michael R. Lowry, Thomas Pressburger, Ian Underwood. 341-355
- Proof Script Pragmatics in IMPSWilliam M. Farmer, Joshua D. Guttman, Mark E. Nadel, F. Javier Thayer. 356-370
- A Mechanization of Strong Kleene Logic for Partial FunctionsManfred Kerber, Michael Kohlhase. 371-385
- Algebraic Factoring and Geometry ProvingDongming Wang. 386-400
- Mechanically Proving Geometry Theorems Using a Combination of Wu s Method and Collins MethodNicholas Freitag McPhee, Shang-Ching Chou, Xiao-Shan Gao. 401-415
- Str+ve and IntegersLarry M. Hines. 416-430
- What is a Proof? (Abstract)Richard Platek. 431
- Termination, Geometry and InvariantsUrsula Martin. 432-434
- Ordered Chaining for Total OrderingsLeo Bachmair, Harald Ganzinger. 435-450
- Simple Termination RevisitedAart Middeldorp, Hans Zantema. 451-465
- Termination Orderings for RipplingDavid A. Basin, Toby Walsh. 466-483
- A Novel Asynchronous Parallelism Scheme for First-Order LogicDavid B. Sturgill, Alberto Maria Segre. 484-498
- Proving with BDDs and Control of InformationJean Goubault. 499-513
- Extended Path-IndexingPeter Graf. 514-528
- Exporting and Refecting Abstract MetamathematicsRobert L. Constable. 529
- Associative-Commutative Deduction with ConstraintsLaurent Vigneron. 530-544
- AC-Superposition with Constraints: No AC-Unifiers NeededRobert Nieuwenhuis, Albert Rubio. 545-559
- The Complexity of Counting Problems in Equational MatchingMiki Hermann, Phokion G. Kolaitis. 560-574
- Representing Proof Transformations for Program OptimizationsPenny Anderson. 575-589
- Exploring Abstract Algebra in Constructive Type TheoryPaul Jackson. 590-604
- Tactic Theorem Proving with Refinement-Tree Proofs and MetavariablesAmy P. Felty, Douglas J. Howe. 605-619
- Unification in an Extensional Lambda Calculus with Ordered Function Sorts and Constant OverloadingPatricia Johann, Michael Kohlhase. 620-634
- Decidable Higher-Order Unification ProblemsChristian Prehofer. 635-649
- Theory and Practice of Minimal Modular Higher-Order E-UnificationOlaf Müller, Franz Weber. 650-664
- A Refined Version of General E-UnificationRolf Socher-Ambrosius. 665-677
- A Completion-Based Method for Mixed Universal and Rigid E-UnificationBernhard Beckert. 678-692
- On Pot, Pans and Pudding or How to Discover Generalised Critical PairsReinhard Bündgen. 693-707
- Semantic Tableaux with Ordering RestrictionsStefan Klingenbeck, Reiner Hähnle. 708-722
- Strongly Analytic Tableaux for Normal Modal LogicsFabio Massacci. 723-737
- Reconstruction Proofs at the Assertion LevelXiaorong Huang. 738-752
- Problems on the Generation of Finite ModelsJian Zhang. 753-757
- Combining Symbolic Computation and Theorem Proving: Some Problems of RamanujanEdmund M. Clarke, Xudong Zhao. 758-763
- SCOTT: Semantically Constrained Otter System DescriptionJohn K. Slaney, Ewing L. Lusk, William McCune. 764-768
- PROTEIN: A PROver with a Theory Extension INterfacePeter Baumgartner, Ulrich Furbach. 769-773
- DELTA - A Bottom-up Preprocessor for Top-Down Theorem Provers - System AbstractJohann Schumann. 774-777
- SETHEO V3.2: Recent Developments - System AbstractChristoph Goller, Reinhold Letz, Klaus Mayr, Johann Schumann. 778-782
- KoMeTWolfgang Bibel, Stefan Brüning, Uwe Egly, Thomas Rath. 783-787
- Omega-MKRP: A Proof Development EnvironmentXiaorong Huang, Manfred Kerber, Michael Kohlhase, Erica Melis, Dan Nesmith, Jörn Richts, Jörg H. Siekmann. 788-792
- leanT:::A:::P: Lean Tableau-Based Theorem Proving (Extended Abstract)Bernhard Beckert, Joachim Posegga. 793-797
- FINDER: Finite Domain Enumerator - System DescriptionJohn K. Slaney. 798-801
- Symlog: Automated Advice in Fitch-style Proof ConstructionFrederic D. Portoraro. 802-806
- KEIM: A Toolkit for Automated DeductionXiaorong Huang, Manfred Kerber, Michael Kohlhase, Erica Melis, Dan Nesmith, Jörn Richts, Jörg H. Siekmann. 807-810
- Elf: A Meta-Language for Deductive Systems (System Descrition)Frank Pfenning. 811-815
- EUODHILOS-II on Top of GNU EpochTakeshi Ohtani, Hajime Sawamura, Toshiro Minami. 816-820
- Pi: an Interactive Derivation Editor for the Calculus of Partial Inductive DefinitionsLars-Henrik Eriksson. 821-825
- Mollusc: A General Proof-Development Shell for Sequent-Based LogicsBradley L. Richards, Ina Kraan, Alan Smaill, Geraint A. Wiggins. 826-830
- KITP-93: An Automated Inference System for Program AnalysisTie-Cheng Wang, Allen Goldberg. 831-835
- SPIKE: a System for Sufficient Completeness and Parameterized Inductive ProofsAdel Bouhoula. 836-840
- Distributed Theorem Proving by PeersMaria Paola Bonacina, William McCune. 841-845