Journal of Automated Reasoning (JAR), Volume 7

Volume 7, Number 1, March 1991

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

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

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

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
  
• Domenico Cantone:
  Decision Procedures for Elementary Sublanguages of Set Theory: X. Multilevel Syllogistic Extended by the Singleton and Powerset Operators. 193-230
  
• Domenico Cantone, Jacob T. Schwartz:
  Decision Procedures for Elementary Sublanguages of Set Theory: XI. Multilevel Syllogistic Extended by Some Elementary Map Constructs. 231-256
  
• Alfredo Ferro:
  Decision Procedures for Elementary Sublanguages of Set Theory: XII. Multilevel Syllogistic Extended with Singleton and Choice Operators. 257-270
  
• Franco Parlamento, Alberto Policriti:
  Decision Procedures for Elementary Sublanguages of Set Theory: XIII. Model Graphs, Reflection and Decidability. 271-284
  

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

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

Volume 7, Number 3, September 1991

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

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

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

Volume 7, Number 4 December 1991

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

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

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

Last update Tue Feb 14 04:19:59 2012 CET by the DBLP Team — Data released under the ODC-BY 1.0 license — See also our legal information page