Abstract is missing.
- The Char-Set Method and Its Applications to Automated ReasoningWu Wen-Tsün. 1-3
- Decidable Call by Need Computations in term Rewriting (Extended Abstract)Irène Durand, Aart Middeldorp. 4-18
- A New Approach for Combining Decision Procedure for the Word Problem, and Its Connection to the Nelson-Oppen Combination MethodFranz Baader, Cesare Tinelli. 19-33
- On Equality Up-to Constraints over Finite Trees, Context Unification, and One-Step RewritingJoachim Niehren, Manfred Pinkal, Peter Ruhrberg. 34-48
- Dedan: A Kernel of Data Structures and Algorithms for Automated Deduction with Equality ClausesRobert Nieuwenhuis, José Miguel Rivero, Miguel Ángel Vallejo. 49-52
- The Clause-Diffusion Theorem Prover Peers-mcd (System Description)Maria Paola Bonacina. 53-56
- Integration of Automated and Interactive Theorem Proving in ILPBernd I. Dahn, Jürgen Gehne, Th. Honigmann, Andreas Wolf. 57-60
- ILF-SETHEO: Processing Model Elimination Proofs for Natural Language OutputAndreas Wolf, Johann Schumann. 61-64
- SETHEO Goes Software Engineering: Application of ATP to Software ReuseBernd Fischer, Johann Schumann. 65-68
- Proving System Correctness with KIV 3.0Wolfgang Reif, Gerhard Schellhorn, Kurt Stenzel. 69-72
- A Practical Symbolic Algorithm for the Inverse Kinematics of 6R Manipulators with Simple GeometryLu Yang, Hongguang Fu, Zhenbing Zeng. 73-86
- Automatic Verification of Cryptographic Protocols with SETHEOJohann Schumann. 87-100
- A Practical Integration of First-Order Reasoning and Decision ProceduresNikolaj Bjørner, Mark E. Stickel, Tomás E. Uribe. 101-115
- Some Pitfalls of LK-to-LJ Translations and How to Avoid ThemUwe Egly. 116-130
- Deciding Intuitionistic Propositional Logic via Translation into Classical LogicDaniel S. Korn, Christoph Kreitz. 131-145
- Lemma Matching for a PTTP-based Top-down Theorem ProverKoji Iwanuma. 146-160
- Exact Kanowledge Compilation in Predicate Calculus: The Partial Achievement CaseOlivier Roussel, Philippe Mathieu. 161-175
- Non-Horn Magic Sets to Incorporate Top-down Inference into Bottom-up Theorem ProvingRyuzo Hasegawa, Katsumi Inoue, Yoshihiko Ohta, Miyuki Koshimura. 176-190
- Alternating Automata: Unifying Truth and Validity Checking for Temporal LogicsMoshe Y. Vardi. 191-206
- Connection-Based Proof Construction in Linear LogicChristoph Kreitz, Heiko Mantel, Jens Otten, Stephan Schmitt. 207-221
- Resource-Distribution via Boolean Constraint (Extended Abstract)James Harland, David J. Pym. 222-236
- Constructing a Normal Form for Property TheoryMary Cryan, Allan Ramsay. 237-251
- Omega: Towards a Mathematical AssistantChristoph Benzmüller, Lassaad Cheikhrouhou, Detlef Fehrer, Armin Fiedler, Xiaorong Huang, Manfred Kerber, Michael Kohlhase, Karsten Konrad, Andreas Meier, Erica Melis, Wolf Schaarschmidt, Jörg H. Siekmann, Volker Sorge. 252-255
- Plagiator - A Learning ProverThomas Kolbe, Jürgen Brauburger. 256-259
- CODE: A Powerful Prover for Problems of Condensed DetachmentDirk Fuchs, Matthias Fuchs. 260-263
- A New Method for Testing Decision Procedures in Modal LogicsFausto Giunchiglia, Marco Roveri, Roberto Sebastiani. 264-267
- Minlog: A Minimal Logic Theorem ProverJohn K. Slaney. 268-271
- SATO: An Efficient Propositional ProverHantao Zhang. 272-275
- Using A Generalisation Critic to Find Bisimulations for Coinductive ProofsLouise A. Dennis, Alan Bundy, Ian Green. 276-290
- A Colored Version of the Lambda-CalculusDieter Hutter, Michael Kohlhase. 291-305
- A Practical Implementation of Simple Consequence Relations Using Inductive DefinitionsSeán Matthews. 306-320
- Soft Typing for Ordered ResolutionHarald Ganzinger, Christoph Meyer, Christoph Weidenbach. 321-335
- A Classification of Non-liftable Orders for ResolutionHans de Nivelle. 336-350
- Hybrid Interactive Theorem Proving Using Nuprl and HOLAmy P. Felty, Douglas J. Howe. 351-365
- Proof Tactics for a Theory of State Machines in a Graphical EnvironmentKatherine A. Eastaughffe, Maris A. Ozols, Anthony Cant. 366-379
- RALL: Machine-Supported Proofs for Relation AlgebraDavid von Oheimb, Thomas F. Gritzner. 380-394
- Nuprl-Light: An Implementation Framework for Higher-Order LogicsJason J. Hickey. 395-399
- XIsabelle: A System DescriptionMaris A. Ozols, Anthony Cant, Katherine A. Eastaughffe. 400-403
- XBarnacle: Making Theorem Provers More AccessibleHelen Lowe, David Duncan. 404-407
- The Tableau Browser SNARKSMathias Kettner, Norbert Eisinger. 408-411
- Jape: A Calculator for Animating Proof-on-PaperRichard Bornat, Bernard Sufrin. 412-415
- Evolving CombinatorsMatthias Fuchs. 416-430
- Partial Matching for Analogy Discovery in Proofs and Counter-ExamplesGilles Défourneaux, Nicolas Peltier. 431-445
- DiaLog: A System for Dialogue LogicJürgen Ehrensberger, Claus Zinn. 446-460