Journal of Automated Reasoning (JAR), Volume 19

Volume 19, Number 1, August 1997

• Jürgen Giesl: Termination of Nested and Mutually Recursive Algorithms. 1-29
• C. A. Johnson: Deduction Trees and the View Update Problem in Indefinite Deductive Databases. 31-85
• Paliath Narendran, Friedrich Otto: Single Versus Simultaneous Equational Unification and Equational Unification for Variable-Permuting Theories. 87-115
• Owen L. Astrachan, Donald W. Loveland: The Use of Lemmas in the Model Elimination Procedure. 117-141

Volume 19, Number 2, October 1997

• Marc-Michel Corsini, Antoine Rauzy: Toupie: The µ-calculus over Finite Domains as a Constraint Language. 143-171
• Karin Hörwein: Structuring Resolution Proofs by Introducing New Lemmata. 173-203
• Peter Baumgartner, Stefan Brüning: A Disjunctive Positive Refinement of Model Elimination and its Application to Subsumption Deletion. 205-262

Volume 19, Number 3, December 1997

• William McCune: Solution of the Robbins Problem. 263-276
• Ricardo Caferra, Nicolas Peltier: A New Technique for Verifying and Correcting Logic Programs. 277-318
• Alan Bundy, Fausto Giunchiglia, Adolfo Villafiorita, Toby Walsh: Abstract Proof Checking: An Example Motivated by an Incompleteness Theorem. 319-346
• David B. Sturgill, Alberto Maria Segre: Nagging: A Distributed, Adversarial Search-Pruning Technique Applied to First-Order Inference. 347-376