Abstract is missing.
- Saturation-Based Theorem Proving: Past Successes and Future Potential (Abstract)Harald Ganzinger. 1
- A Resolution Theorem Prover for Intuitonistic LogicTanel Tammet. 2-16
- Proof-Terms for Classical and Intuitionistic Resolution (Extended Abstract)Eike Ritter, David J. Pym, Lincoln A. Wallen. 17-31
- Proof-Search in Intuitionistic Logic with Equality, or Back to Simultaneous Rigid E-UnificationAndrei Voronkov. 32-46
- Extensions to a Generalization Critic for Inductive ProofAndrew Ireland, Alan Bundy. 47-61
- Learning Domain Knowledge to Improve Theorem ProvingJörg Denzinger, Stephan Schulz. 62-76
- Patching Faulty ConjecturesMartin Protzen. 77-91
- Internal Analogy in Theorem ProvingErica Melis, Jon Whittle. 92-105
- Termination of Theorem Proving by ReuseThomas Kolbe, Christoph Walther. 106-120
- Termination of Algorithms over Non-freely Generated Data TypesClaus Sengler. 121-135
- ABSFOL: A Proof Checker with AbstractionFausto Giunchiglia, Adolfo Villafiorita. 136-140
- SPASS & FLOTTER Version 0.42Christoph Weidenbach, Bernd Gaede, Georg Rock. 141-145
- The Design of the CADE-13 ATP System CompetitionChristian B. Suttner, Geoff Sutcliffe. 146-160
- SCAN - Elimination of Predicate QuantifiersHans Jürgen Ohlbach. 161-165
- GEOTHER: A Geometry Theorem ProverDongming Wang. 166-170
- Structuring Metatheory on Inductive DefinitionsDavid A. Basin, Seán Matthews. 171-185
- An Embedding of Ruby in IsabelleOle Rasmussen. 186-200
- Mechanical Verification of Mutually Recursive ProceduresPeter V. Homeier, David F. Martin. 201-215
- FasTraC: A Decentralized Traffic Control System Based on Logic ProgrammingGiovanni Felici, Giovanni Rinaldi, Klaus Truemper. 216-220
- Presenting Machine-Found ProofsXiaorong Huang, Armin Fiedler. 221-225
- MUltlog 1.0: Towards an Expert System for Many-Valued LogicsMatthias Baaz, Christian G. Fermüller, Gernot Salzer, Richard Zach. 226-230
- CtCoq: A System PresentationJanet Bertot, Yves Bertot. 231-234
- An Introduction to Geometry ExpertShang-Ching Chou, Xiao-Shan Gao, Jing-Zhong Zhang. 235-239
- SiCoTHEO: Simple Competitive Parallel Theorem ProversJohann Schumann. 240-244
- What Can We Hope to Achieve From Automated Deduction? (Abstract)Dana S. Scott. 245
- Unification Algorithms Cannot be Combined in Polynomial TimeMiki Hermann, Phokion G. Kolaitis. 246-260
- Unification and Matching Modulo NilpotenceQing Guo, Paliath Narendran, David A. Wolfram. 261-274
- An Improved Lower Bound for the Elementary Theories of TreesSergei G. Vorobyov. 275-287
- INKA: The Next GenerationDieter Hutter, Claus Sengler. 288-292
- XRay: A Prolog Technology Theorem Prover for Default Reasoning: A System DescriptionTorsten Schaub, Stefan Brüning, Pascal Nicolas. 293-297
- IMPS: An Updated System DescriptionWilliam M. Farmer, Joshua D. Guttman, F. Javier Thayer. 298-302
- The Tableau-based Theorem Prover ::3::T:::A:::P Version 4.0Bernhard Beckert, Reiner Hähnle, Peter Oel, Martin Sulzmann. 303-307
- System Description: Generating Models by SEMJian Zhang, Hantao Zhang. 308-312
- Optimizing Proof Search in Model EliminationJohn Harrison. 313-327
- An Abstract Machine for Fixed-Order Dynamically Stratified ProgramsKonstantinos F. Sagonas, Terrance Swift, David Scott Warren. 328-342
- Unification in Pseudo-Linear Sort Theories is DecidableChristoph Weidenbach. 343-357
- Theorem Proving with Group Presentations: Examples and QuestionsUrsula Martin. 358-372
- Transforming Termination by Self-LabellingAart Middeldorp, Hitoshi Ohsaki, Hans Zantema. 373-387
- Theorem Proving in Cancellative Abelian Monoids (Extended Abstract)Harald Ganzinger, Uwe Waldmann. 388-402
- On the Practical Value of Different Definitional Translations to Normal FormUwe Egly, Thomas Rath. 403-417
- Converting Non-Classical Matrix Proofs into Sequent-Style SystemsStephan Schmitt, Christoph Kreitz. 418-432
- Efficient Model Generation through CompilationHeribert Schütz, Tim Geisler. 433-447
- Algebra and Automated DeductionSteve Linton, Ursula Martin, Péter Pröhle, Duncan Shand. 448-462
- On Shostak s Decision Procedure for Combinations of TheoriesDavid Cyrluk, Patrick Lincoln, Natarajan Shankar. 463-477
- Ground Resolution with Group Computations on Semantic SymmetriesThierry Boy de la Tour. 478-492
- A New Method for Knowledge Compilation: The Achievement by Cycle SearchOlivier Roussel, Philippe Mathieu. 493-507
- Rewrite Semantics for Production Rule Systems: Theory and ApplicationsWayne Snyder, James G. Schmolze. 508-522
- Experiments in the Heuristic Use of Past Proof ExperienceMatthias Fuchs. 523-537
- Lemma Discovery in Automated InductionDeepak Kapur, Mahadevan Subramaniam. 538-552
- Advanced Indexing Operations on Substitution TreesPeter Graf, Christoph Meyer. 553-567
- Semantic Trees Revisited: Some New Completeness ResultsChristian G. Fermüller. 568-582
- Building Decision Procedures for Modal Logics from Propositional Decision Procedure - The Case Study of Modal KFausto Giunchiglia, Roberto Sebastiani. 583-597
- Resolution-Based Calculi for Modal and Temporal LogicsAndreas Nonnengart. 598-612
- Tableaux and Algorithms for Propositional Dynamic Logic with ConverseGiuseppe De Giacomo, Fabio Massacci. 613-627
- Reflection of Formal Tactics in a Deductive Reflection FrameworkHarald Rueß. 628-642
- Walther RecursionDavid A. McAllester, Kostas Arkoudas. 643-657
- Proof Search with Set Variable Instantiation in the Calculus of ConstructionsAmy P. Felty. 658-672
- Search Strategies for Resolution in Temporal LogicsClare Dixon. 673-687
- Optimal Axiomatizations for Multiple-Valued Operators and Quantifiers Based on Semi-latticesGernot Salzer. 688-702
- Grammar Specification in Categorial Logics and Theorem ProvingSaturnino F. Luz-Filho. 703-717
- Path Indexing for AC-TheoriesPeter Graf. 718-732
- More Church-Rosser Proofs (in Isabelle/HOL)Tobias Nipkow. 733-747
- Partitioning Methods for Satisfiability Testing on Large FormulasTai Joon Park, Allen Van Gelder. 748-762