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 BibTeX
• C. A. Johnson: Deduction Trees and the View Update Problem in Indefinite Deductive Databases. 31-85 BibTeX
• Paliath Narendran, Friedrich Otto: Single Versus Simultaneous Equational Unification and Equational Unification for Variable-Permuting Theories. 87-115 BibTeX
• Owen L. Astrachan, Donald W. Loveland: The Use of Lemmas in the Model Elimination Procedure. 117-141 BibTeX

Volume 19, Number 2, October 1997

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

Volume 19, Number 3, December 1997

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