| The Char-Set Method and Its Applications to Automated Reasoning | p. 1 |
| Decidable Call by Need Computations in Term Rewriting | p. 4 |
| A New Approach for Combining Decision Procedures for the Word Problem, and Its Connection to the Nelson-Oppen Combination Method | p. 19 |
| On Equality Up-to Constraints over Finite Trees, Context Unification, and One-Step Rewriting | p. 34 |
| Dedam: A Kernel of Data Structures and Algorithms for Automated Deduction with Equality Clauses | p. 49 |
| The Clause-Diffusion Theorem Prover Peers-mcd | p. 53 |
| Integration of Automated and Interactive Theorem Proving in ILF | p. 57 |
| ILF-SETHEO: Processing Model Elimination Proofs for Natural Language Output | p. 61 |
| SETHEO Goes Software Engineering: Application of ATP to Software Reuse | p. 65 |
| Proving System Correctness with KIV 3.0 | p. 69 |
| A Practical Symbolic Algorithm for the Inverse Kinematics of 6R Manipulators with Simple Geometry | p. 73 |
| Automatic Verification of Cryptographic Protocols with SETHEO | p. 87 |
| A Practical Integration of First-Order Reasoning and Decision Procedures | p. 101 |
| Some Pitfalls of LK-to-LJ Translations and How to Avoid Them | p. 116 |
| Deciding Intuitionistic Propositional Logic via Translation into Classical Logic | p. 131 |
| Lemma Matching for a PTTP-based Top-down Theorem Prover | p. 146 |
| Exact Knowledge Compilation in Predicate Calculus: The Partial Achievement Case | p. 161 |
| Non-Horn Magic Sets to Incorporate Top-down Inference into Bottom-up Theorem Proving | p. 176 |
| Alternating Automata: Unifying Truth and Validity Checking for Temporal Logics | p. 191 |
| Connection-Based Proof Construction in Linear Logic | p. 207 |
| Resource-Distribution via Boolean Constraints | p. 222 |
| Constructing a Normal Form for Property Theory | p. 237 |
| [Omega]MEGA: Towards a Mathematical Assistant | p. 252 |
| PLAGIATOR: A Learning Prover | p. 256 |
| CODE: A Powerful Prover for Problems of Condensed Detachment | p. 260 |
| A New Method for Testing Decision Procedures in Modal Logics | p. 264 |
| MINLOG: A Minimal Logic Theorem Prover | p. 268 |
| SATO: An Efficient Propositional Prover | p. 272 |
| Using a Generalisation Critic to Find Bisimulations for Coinductive Proofs | p. 276 |
| A Colored Version of the [lambda]-Calculus | p. 291 |
| A Practical Implementation of Simple Consequence Relations Using Inductive Definitions | p. 306 |
| Soft Typing for Ordered Resolution | p. 321 |
| A Classification of Non-Liftable Orders for Resolution | p. 336 |
| Hybrid Interactive Theorem Proving Using Nuprl and HOL | p. 351 |
| Proof Tactics for a Theory of State Machines in a Graphical Environment | p. 366 |
| RALL: Machine-Supported Proofs for Relation Algebra | p. 380 |
| Nuprl-Light: An Implementation Framework for Higher-Order Logics | p. 395 |
| XIsabelle: A System Description | p. 400 |
| XBarnacle: Making Theorem Provers More Accessible | p. 404 |
| The Tableau Browser SNARKS | p. 408 |
| Jape: A Calculator for Animating Proof-on-Paper | p. 412 |
| Evolving Combinators | p. 416 |
| Partial Matching for Analogy Discovery in Proofs and Counter-examples | p. 431 |
| DIALOG: A System for Dialogue Logic | p. 446 |
| Author Index | p. 461 |
| Table of Contents provided by Blackwell. All Rights Reserved. |