Journal of Automated Reasoning (JAR), Volume 7

Volume 7, Number 1, March 1991

• Donald W. Loveland: Near-Horn Prolog and Beyond. 1-26 BibTeX
• Peter Padawitz: Inductive Expansion: A Calculus for Verifying and Synthesizing Functional and Logic Programs. 27-103 BibTeX

• Larry Wos: The Problem of Finding a Restriction Strategy More Effective Than the Set of Support Strategy. 105-107 BibTeX

• Matt Kaufmann: Generalization in the Presence of Free Variables: A Mechanically-Checked Correctness Proof for one Algorithm. 109-158 BibTeX

Volume 7, Number 2, June 1991

• Wu Wen-Tsün: Mechanical Theorem Proving of Differential Geometries and Some of its Applications in Mechanics. 171-191 BibTeX
• Domenico Cantone: Decision Procedures for Elementary Sublanguages of Set Theory: X. Multilevel Syllogistic Extended by the Singleton and Powerset Operators. 193-230 BibTeX
• Domenico Cantone, Jacob T. Schwartz: Decision Procedures for Elementary Sublanguages of Set Theory: XI. Multilevel Syllogistic Extended by Some Elementary Map Constructs. 231-256 BibTeX
• Alfredo Ferro: Decision Procedures for Elementary Sublanguages of Set Theory: XII. Multilevel Syllogistic Extended with Singleton and Choice Operators. 257-270 BibTeX
• Franco Parlamento, Alberto Policriti: Decision Procedures for Elementary Sublanguages of Set Theory: XIII. Model Graphs, Reflection and Decidability. 271-284 BibTeX

• Peter B. Andrews: More on the Problem of Finding a Mapping between Clause Representation and Natural Deduction Representation. 285-286 BibTeX

• Art Quaife: Unsolved Problems in Elementary Number Theory. 287-300 BibTeX

Volume 7, Number 3, September 1991

• Alan Bundy, Frank van Harmelen, Jane Hesketh, Alan Smaill: Experiments with Proof Plans for Induction. 303-324 BibTeX
• Rolf Socher: Optimizing the Clausal Normal Form Transformation. 325-336 BibTeX
• Danny De Schreye, Bern Martens, Gunther Sablon, Maurice Bruynooghe: Compiling Bottom-up and Mixed Derivations into Top-down Executable Logic Programs. 337-358 BibTeX
• Allan Ramsay: Generating Relevant Models. 359-368 BibTeX
• Werner Nutt: The Unification Hierarchy is Undecidable. 369-381 BibTeX
• Tong Gao Tang: Programming in Temporal-Nonmonotonic Reasoning. 383-401 BibTeX
• Yishai A. Feldman, Charles Rich: Pattern-Directed Invocation with Changing Equations. 403-433 BibTeX

• Larry Wos: The Problem of Choosing the Type of Subsumption to Use. 435-438 BibTeX

• Matthew Wilding: Proving Matijasevich's Lemma with a Default Arithmetic Strategy. 439-446 BibTeX

Volume 7, Number 4 December 1991

• Michael A. McRobbie: Automated Reasoning and Nonclassical Logics: Introduction. 447-451 BibTeX
• John K. Slaney: The Ackermann Constant Theorem: A Computer-Assisted Investigation. 453-474 BibTeX
• Paul Pritchard: Algorithms for Finding Matrix Models of Propositional Calculi. 475-487 BibTeX
• Laurent Catach: TABLEAUX: A General Theorem Prover for Modal Logics. 489-510 BibTeX
• Dov M. Gabbay, Frank Kriwaczek: A Family of Goal Directed Theorem Provers Based on Conjunction and Implication: Part I. 511-536 BibTeX
• Dick De Jongh, Lex Hendriks, Gerard R. Renardel de Lavalette: Computations in Fragments of Intuitionistic Propositional Logic. 537-561 BibTeX
• A. W. Bollen: Relevant Logic Programming. 563-585 BibTeX
• Grigori Mints, Tanel Tammet: Condensed Detachment is Complete for Relevance Logic: A Computer-Aided Proof. 587-596 BibTeX
• Robert K. Meyer, Martin W. Bunder, Lawrence Powers: Implementing the `Fool's Model' of Combinatory Logic. 597-630 BibTeX

• Larry Wos: The Problem of Choosing the Representation, Inference Rule, and Strategy. 631-634 BibTeX

• Paul B. Thistlewaite, Michael A. McRobbie: Approaching Hard Non-Classical Problems. 635-637 BibTeX