Journal of Automated Reasoning (JAR), Volume 2

Volume 2, Number 1, 1986

Bruce D. Parrello, Waldo C. Kabat: Job-Shop Scheduling Using Automated Reasoning: A Case Study of the Car-Sequencing Problem. 1-42
Werner Dilger, Agnes Janson: Intelligent Backtracking in Deduction Systems by Means of Extended Unification Graphs. 44-62
Lawrence C. Paulson: Proving Termination of Normalization Functions for Conditional Experessions. 63-74
Wolfram Büttner: Unification in Datastructure Multisets. 75-88

Problem Corner

Mark E. Stickel: Schubert's Steamroller Problem: Formulation and Solutions. 89-101

Alan Bundy: Correctness Criteria of Some Algorithms for Uncertain Reasoning Using Incidence Calculus. 109-126
Thomas Kramer: Automated Analysis of Operators on State Tables: A Technique for Intelligent Search. 127-153
C. Aquilano, Roberto Barbuti, P. Bocchetti, Maurizio Martelli: Negation as Failure. Completeness of the Query Evaluation Process for Horn Clause Programs with Recursive Definitions. 155-170
David A. Plaisted: A Decision Procedure for Combinations of Propositional Temporal Logic and Other Specialized Theories. 171-190

Problem Corner

Francis Jeffry Pelletier: Seventy-Five Problems for Testing Automatiac Theorem Provers. 191-216 , Errata: JAR 4(2): 235-236 (1988)

Wu Wen-Tsün: Basic Principles of Mechanical Theorem Proving in Elementary Geometries. 221-252
Shang-Ching Chou, William F. Schelter: Proving Geometry Theorems with Rewrite Rules. 253-273
Manfred Schmidt-Schauß: Unification under Associativity and Idempotence is of Type Nullary. 277-281
Franz Baader: The Theory of Idempotent Semigroups is of Unification Type Zero. 283-286

Problem Corner:

Helder Coelho, Luís Moniz Pereira: Automated Reasoning in Geometry Theorem Proving with Prolog. 329-390
Jia-Huai You, P. A. Subrahmanyam: A Class of Confluent Term Rewriting Systems and Unification. 391-418
Barney Glickfeld, Ross A. Overbeek: A Foray Into Combinatory Logic. 419-431