Journal of Automated Reasoning 7 (1991) Contents to Volume 7 Volume 7 No.1 March 199] Publisher’s Announcement DONALD W. LOVELAND / Near-Horn Prolog and Beyond PETER PADAWITZ / Inductive Expansion: A Calculus for Verifying and Synthesizing Functional and Logic Programs Basic Research Problems: LARRY WOS / The Problem of Finding a Restriction Strategy More Effective than the Set of Support Strategy Problem Corner: MATT KAUFMANN / Generalization in the Presence of Free Variables: A Mechanically-Checked Correctness Proof for one Algorithm Book Reviews: Shang-Ching Chou: Mechanical Geometry Theorem Proving (RICK STEVENS) Deepak Kapur and Joseph Mundy (Eds.): Geometric Reasoning (RICK STEVENS) Guy E. Blelloch: Vector Models for Data Parallel Computing (RICK STEVENS) M. E. Stickel (Ed.): CADE-10 Proceedings, Lecture Notes in Artificial Intelligence Vol. 449 (RICK STEVENS) Errata: Timothy Stokes: ‘Grébner Bases in Exterior Algebra’, J. Automated Reason- ing 6, 233-250 (1990) Addresses of Editorial Board Volume 7 No.2 June 199] Special Issue on NEW TRENDS IN AUTOMATED REASONING Edited by VLADIMIR LIFSCHITZ and ALFREDO FERRO JOURNAL OF AUTOMATED REASONING ALFREDO FERRO / Introduction 169 WU WEN-TSUN / Mechanical Theorem Proving of Differential Geometries and Some of its Applications in Mechanics 171 D. CANTONE / Decision Procedures for Elementary Sublanguages of Set Theory: X. Multilevel Syllogistic Extended by the Singleton and Powerset Operators 193 D. CANTONE and J.T. SCHWARTZ / Decision Procedures for Elementary Sublanguages of Set Theory: XI. Multilevel Syllogistic Extended by Some Elementary Map Constructs A. FERRO / Decision Procedures for Elementary Sublanguages of Set Theory: XII. Multilevel Syllogistic Extended with Singleton and Choice Operators FRANCO PARLAMENTO and ALBERTO POLICRITI / Decision Procedures for Elementary Sublanguages of Set Theory: XIII. Model Graphs, Reflection and Decidability Basic Research Problems: PETER B. ANDREWS / More on the Problem of Finding a Mapping between Clause Representation and Natural-Deduction Representation Problem Corner: ART QUAIFE / Unsolved Problems in Elementary Number Theory Volume 7 No.3 September 199] LARRY WOS / A Well-Kept Secret of History ALAN BUNDY, FRANK VAN HARMELEN, JANE HESKETH, and ALAN SMAILL / Experiments with Proof Plans for Induction ROLF SOCHER / Optimizing the Clausal Normal Form Transformation DANNY DE SCHREYE, BERN MARTENS, GUNTHER SABLON, and MAURICE BRUYNOOGHE / Compiling Bottom-up and Mixed Derivations into Top-down Executable Logic Programs ALLAN RAMSAY / Generating Relevant Models WERNER NUTT / The Unification Hierarchy is Undecidable TONG GAO TANG / Programming in Temporal-Nonmonotonic Reasoning YISHAI A. FELDMAN and CHARLES RICH / Pattern-Directed Invocation with Changing Equations Basic Research Problems: LARRY WOS / The Problem of Choosing the Type of Subsumption to Use INDEX FOR VOLUME 7 Problem Corner: MATTHEW WILDING / Proving Matijasevich’s Lemma with a Default Arithmetic Strategy 439 Volume 7 No.4 December 1991 Special Issue on AUTOMATED REASONING AND NONCLASSICAL LOGICS Edited by MICHAEL A. McROBBIE Institute of Advanced Studies, Australian National University MICHAEL A. McROBBIE / Automated Reasoning and Nonclassical Logics: Introduction JOHN K. SLANEY / The Ackermann Constant Theorem: A Computer-Assisted Investigation PAUL PRITCHARD / Algorithms for Finding Matrix Models of Propositional Calculi LAURENT CATACH / TABLEAUX: A General Theorem Prover for Modal Logics DOV M. GABBAY and FRANK KRIWACZEK / A Family of Goal Directed Theorem Provers Based on Conjunction and Implication: Part 1 DICK DE JONGH, LEX HENDRIKS, and GERARD R. RENARDEL DE LAVALETTE / Computations in Fragments of Intuitionistic Propositional Logic A. W. BOLLEN / Relevant Logic Programming GRIGORI MINTS and TANEL TAMMET / Condensed Detachment is Complete for Relevance Logic: A Computer-Aided Proof ROBERT K. MEYER, MARTIN W. BUNDER, and LAWRENCE POWERS / Implementing the ‘Fool’s Model’ of Combinatory Logic Basic Research Problems: LARRY WOS / The Problem of Choosing the Representation, Inference Rule, and Strategy Problem Corner: PAUL B. THISTLEWAITE and MICHAEL A. McROBBIE / Approaching Hard Non-Classical Problems Author Index to Volume 7 Subject Index to Volume 7