JOURNAL OF AUTOMATED REASONING

For aims and scope, submission of papers information and ordering
information, see file jars.inf.

			CONTENTS VOLUME 10

ISSUE 2, April 1993

- Autoepistemic circumspection and logic programming
	L.Y. Yuan, J.-H. You
- Automated reasoning in differential geometry and mechanics using the
    characteristic set method: Part I. An improved version of Ritt-Wu's
    decomposition algorithm
	S.-C. Chou, X.-S. Gao
- Automated reasoning in differential geometry and mechanics using the
    characteristic set method: Part II. Mechanical theorem proving
	S.-C. Chou, X.-S. Gao
- A semantical framework for supporting subjective and conditional
    probabilities in deductive databases
	R. Ng, V.S. Subrahmanian
- First-order syntactic characterizations of minimal entailment,
  domain-minimal entailment, and herbrand entailment
	M.A. Suchenek
- Gentzen-type systems, resolution and tableaux
	A. Avron
- Basic research problems:
    The problem of selecting an approach based on prior success
	L. Wos
- Book review:
    A. Desrochers: Intelligent robotic systems for space exploration
	C. Ashbachter

ISSUE 1, February 1993

- Studies in automated reasoning:
    Single axioms for groups and Abelian groups with various operations
	W.W. McCune
- Experimenting with Isabelle in ZF set theory
	P.A.J. Noel
- Fuzzy operator logic and fuzzy resolution
	T.J. Weigert, J.-P. Tsai, X. Liu
- What holds in a context?
	F. Corella
- Flatterms, discrimination nets, and fast term rewriting
	J. Christian
- Simplification in a satisfiability checker for VLSI applications
	F. Vlach
- Basic research problems:
    The problem of automated theorem finding
	L. Wos
- Addresses of editorial board

		CONTENTS VOLUME 9

ISSUE 3, 1992

- Transition to the future
	L. Wos
- Single axioms for gruops
	K. Kunen
- Using typed lambda calculus to implement formal systems on a machine
	A. Avron, F. Honsell, I.A. Mason, R. Pollack
- An extension of the Boyer-Moore theorem prover to support first-order
    quantification
	M. Kaufmann
- On Fourier's algorithm for linear arithmetic constraints
	J.-L. Lassez, M.J. Maher
- A note on the parallel complexity of anti-unification
	G.M. Kuper, K.W. McAloon, K.V. Palem, K.J. Perry
- Efficient parallel term matching and anti-unification
	A.L. Delcher, S. Kasif
- Basic research problems:
    The problem of demodulating across argument and literal boundaries
	L. Wos
- Basic Review:
    L. Somb‚, Reasoning under incomplete information in artificial intelligence
	S. Parsons
- Author index to volume 9
- Subject index to volume 9

ISSUE 2, October 1992

- Note on McCune's article on discrimination trees
	L. Wos
- Experiments with discrimination-tree indexing and path indexing for term
    retrieval
	W. McCune
- Hilbert's tenth problem is of unification type zero
	M. Franzen
- A logic for reasoning with inconsistency
	M. Kifer, E.L. Lozinskii
- Uncertainty management with imprecise knowledge with application to design
	D.E. Brown, W.J. Markert
- CLP (R) and some electrical engineering problems
	N. Heintze, S. Michaylov, P. Stuckey
- Complexity of unification problems with associative-communitative operators
	D. Kapur, P. Narendran

ISSUE 1, August 1992

- Studies in automated reasoning:
    Automated discovery of new axiomatizations of the left group and right
      group calculi
	W.W. McCune
- Eliminating duplication with the hyper-linking strategy
	S.-J. Lee, D.A. Plaisted
- Recognizing unnecessary clauses in resolution based systems
	D. Benanav
- How to avoid the derivation of redundant clauses in reasoning systems
	R. Socher-Ambrosius
- Tableaux and sequent calculus for minimal entailment
	N. Olivetti
- Basic research problems:
    The problem of demodulation during inference rule application
	L. Wos

			CONTENTS VOLUME 8

ISSUE 3, June 1992

- Gazing: An approach to the problem of definition and lemma use
	D. Barker-Plummer
- Stable and extension class theory for logic programs and default logics
	C.R. Baral, V.S. Subrahmanian
- Comparing parameter schemes for propositional reasoning: An empirical study
	R.J. Hall
- Automatically identifying the asymptotic behavior of nonlinear singularly
  perturbed boundary value problems
	M.F. Russo, R.L. Peskin
- Basic research problems:
    The problem of reasoning from inequalities
	L. Wos
- Author index to volume 8
- Subject index to volume 8

ISSUE 2, April 1992

- A parallel theorem prover for non-horn clauses
	S. Bose, E.M. Clarke, D.E. Long, S. Michaylov
- SETHEO: A high-performance theorem prover
	R. Letz, J. Schumann, S. Bayerl, W. Bibel
- The linked inference principle, I: The formal treatment
	R. Veroff, L. Wos
- An integral theorem prover and the role of proof planning
	J.D. Baker, S. Zand-Biglari
- SLDNF-resolution with equality
	J.C. Shepherdson
- Basic research problems:
    The problem of choosing between using and avoiding equality predicates
	L. Wos

ISSUE 1, February 1992

- Publisher's announcement
- A section is born: Studies in automated reasoning
	L. Wos
- Studies in automated reasoning:
    A mechanical proof of quadratic reciprocity
	D.M. Russinoff
- Exploitation of parallel processing for implementing high-performance
  deduction systems
	A. Jindal, R. Overbeek, W.C. Kabat
- A technical note on AC-unification. The number of minimal unifiers of
  the equation ax1 + ... + axp = AC by1 + ... + byq
	E. Domenjoud
- Completeness of a prover for dense linear orders
	L.M. Hines
- An inexact reasoning algorithm based on fuzzy rule matrix transformations
	S.-M. Chen, J.-S. Ke, J.-F. Chang
- Automated deduction in von Neumann-Bernays-G”del set theory
	A. Quaife
- Addresses of editorial board

			CONTENTS VOLUME 7

ISSUE 4, December 1991
SPECIAL ISSUE ON AUTOMATED REASONING AND NONCLASSICAL LOGICS

- Automated reasoning and nonclassical logics: Introduction
	M.A. McRobbie
- The Ackermann constant theorem: A computer-assisted investigation
	J.K. Slaney
- Algorithms for finding matrix models of propositional calculi
	P. Pritchard
- TABLEAUX: A general theorem prover for modal logics
	L. Catach
- A family of goal directed theorem provers based on conjunction and
  implication: Part I
	D.M. Gabbay, F. Kriwaczek
- Computations in fragments of intuitionistic propositional logic
	D. de Jongh, L. Hendriks, G.R. Renardel de Lavallette
- Relevant logic programming
	A.W. Bollen
- Condensed detachment is complete for relevance logic: A computer-aided
    proof
	G. Mints, T. Tammet
- Implementing the Fool's Model of combinatory logic
	R.K. Meyer, M.W. Bunder, L. Powers
- Basic research problems:
    The problem of choosing the representation, inference rule, and strategy
	L. Wos
- Problem corner:
    Approaching hard non-classical problems
	P.B. Thistlewaite, M.A. McRobbie
- Author index to volume 7
- Subject index to volume 7

ISSUE 3, September 1991

- A well-kept secret of history
	L. Wos
- Experiments with proof plans for induction
	A. Bundy, F. van Harmelen, J. Hesketh, A. Smaill
- Optimizing the clausal normal form transformation
	R. Socher
- Compiling bottom-up and mixed derivations into top-down executable logic
  programs
	D. de Schreye, B. Martens, G. Sablon, M. Bruynooghe
- Generating relevant models
	A. Ramsay
- The unification hierarchy is undecidable
	W. Nutt
- Programming in temporal-nonmonotonic reasoning
	T.G. Tang
- Pattern-directed invocation with changing equations
	Y.A. Feldman, C. Rich
- Basic research problem:
    The problem of choosing the type of subsumption to use
	L. Wos
- Problem corner:
    Proving Matijasevich's lemma with a default arithmetic system
	M. Wilding

ISSUE 2, June 1991
SPECIAL ISSUE ON NEW TRENDS IN AUTOMATED REASONING

- Introduction
	A. Ferro
- Mechanical theorem proving of differential geometries and some of its
  applications in mechanics
	W. Wen-Tsun
- Decision procedures for elementary sublanguages of set theory: X. Multilevel
  syllogistic extended by the singleton and powerset operators
	D. Cantone
- Decision procedures for elementary sublanguages of set theory: XI. Multilevel
  sylllogistic extended by some elementary map constructs
	D. Cantone, J.T. Schwartz
- Decision procedures for elementary sublanguages of set theory: XII. Multilevel
  syllogistic extended with singleton and choice operators
	A. Ferro
- Decision procedures for elementary sublanguages of set theory: XIII. Model
  graphs, reflection and decidability
	F. Parlamento, A. Policriti
- Basic research problems:
    More on the problem of finding a mapping between clause representation
    and natural-deduction representation
	P.B. Andrews
- Problem corner:
    Unsolved problems in elementary number theory
	A. Quaife

ISSUE 1, March 1991

- Publishers announcement
- Near-horn prolog and beyond
	D.W. Loveland
- Inductive expansion: A calculus for verifying and synthesizing functional and
  logic programs
	P. Padawitz
- Basic research problems:
    The problem of finding a restriction strategy more effective than the set
    of support strategy
	L. Wos
- Problem corner:
    Generalization in the presence of free variables: A mechanically-checked
    correctness proof for one algorithm
	M. Kaufmann
- Book review:
    S.-C. Chou: Mechanical geometry theorem proving
	R. Stevens
    D. Kapur and J. Mundy (eds.): Geometric reasoning
	R. Stevens
    G.E. Blelloch: Vector models for data parallel computing
	R. Stevens
    M.E. Stickel (ed.): CADE-10 proceedings, lecture notes in artificial
      intelligence vol. 449
	R. Stevens
- Errata:
    T. Stokes: Gr”bner bases in exterior algebra, J. Automated Reasoning
      6, 233-250 (1990)
- Addresses of editorial board

			CONTENTS VOLUME 6

ISSUE 4, December 1990

- Publisher's announcement
- A decidable first-order logic for knowledge representation
	P.F. Patel-Schneider
- A sequenty-style model elimination strategy and a positive refinement
	D.A. Plaisted
- Transcendental functions and mechanical theorem proving in elementary
    geometries
	X. Gao
- Interest driven suppositional reasoning
	J.L. Pollock
- Basic research problems:
    The problem of choosing between predicate and function notation for
    problem representation
	L. Wos
- Problem corner:
    Robbins Algebra: Conditions that make a near-Boolean algebra Boolean
	S. Winker
- Call for papers
- Author index to volume 6
- Subject index to volume 6

ISSUE 3, September 1990

- Gr”bner bases in exterior algebra
	T. Stokes
- Computer proofs in group theory
	Y. Yu
- Short proofs of the pigeonhole formulas based on the connection method
	W. Bibel
- Interweaving knowledge extracting, organizing and evaluating: a concrete
  design for preventing logic and structure bugs while interviewing experts
	J.S. di Piazza
- Equivalence of propositional prolog programs
	H. Kleine Bning, U. L”wen, S. Schmitgen
- Basic research problems:
    The problem of finding a semantic strategy for focusing inference rules
	L. Wos
- Problem corner:
    Challenge problems in elementary calculus
	W.W. Bledsoe

ISSUE 2, June 1990

- Editorial announcement
- Structure sharing for quantified terms: Fundamentals
	J. Staples, P.J. Robinson
- Protected completions of first-order general logic programs
	J.J. Lu, V.S. Subrahmanian
- The automation of syllogistic. II. Optimization and complexity issues
	D. Cantone, E.G. Omodeo, A. Policriti
- Decision procedures for elementary sublanguages of set theory. XV. Multilevel
  syllogistic extended by the predicate finite and the operators singleton
  and Pred<
	D. Cantone, V. Cutello
- A procedure to prove statements in differential geometry
	G. Carr… Ferro, G. Gallo
- Basic research problems:
    The problem of finding a mapping between clause representation and
    natural-deduction representation
	L. Wos
- Problem corner:
    Meeting the challenge of fifty years of logic
	L. Wos

ISSUE 1, March 1990

- Strategies for modal resolution: Results and problems
	Y. Auffray, P. Enjalbert, J.-J. Hebrard
- On the recursive decomposition ordering with lexico-graphical status and
  other related orderings
	P. Lescanne
- Replacing unification by constraint satisfaction to improve logic program
  expressiveness
	J.W. Roach, R. Sundararajan, L.T. Watson
- Basic research problems:
    The problem of choosing between logic programming and general-purpose
    automated reasoning
	L. Wos
- Problem corner:
    Automated proofs of the moufang identities in alternative rings
	S. Anantharaman, J. Hsiang
- Addresses of editorial board

			CONTENTS VOLUME 4

ISSUE 4, december 1988

- A prolog technology theorem prover: implementation by an extended prolog
  compiler
	M.E. Stickel
- Unification in Boolean rings
	U. Martin, T. Nipkow
- Inferring negative information from disjunctive databases
	K.A. Ross, R.W. Topor
- A new reduction rule for the connection graph proof procedure
	K.H. Munch
- Inference rules using local contexts
	L.G. Monk
- Basic research problems:
    The problems of self-analytically choosing the weights 
	L. Wos
- Problem corner:
    Opening the AC-unification race
	H.-J. Brckert, A. Herold, D. Kapur, J.H. Siekmann, M.E. Stickel,
	M. Tepp, H. Zhang
- Author index to volume 4
- Subject index to volume 4

ISSUE 3, September 1988

- An introduction to Wu's method for mechanical theorem proving in geometry
	S.-C. Chou
- A lambda-unifiability test for set theory
	S.C. Bailin
- Non-horn clause logic programming without contrapositives
	D.A. Plaisted
- Basic research problems:
    The problem of self-analytically choosing the set of support
	L. Wos
- Problem corner:
    Proving equivalence of different axiomatizations of free groups
	D. Kapur, H. Zhang

ISSUE 2, June 1988

- The addition of bounded quantification and partial functions to a
  computational logic and its theorem prover
	R.S. Boyer, J.S. Moore
- Mechanical procedure for proof construction via closed terms in typed
  lambda calculus
	M. Zaionic
- First-order modal tableux
	M. Fitting
- Basic research problems:
    The problem of explaining the disparate performance of hyperresolution
    and paramodulation
	L. Wos
- Problem corner:
    Automated proofs of L”b's theorem and G”del's two incompleteness theorems
	A. Quaife
- Book review:
    L. Wos: Automated Reasoning: 33 basic research problems
	R. Overbeek
- Errata:
    F.J. Pelletier / 75 problems for testing automatic theorem provers, J.
    automated reasoning 2, 191-216 (1986)

ISSUE 1, March 1988

- Publisher's announcement
- Model minimization - an alternative to circumscription
	J. Hintikka
- Meta-level inference two applications
	A. Bundy, L. Sterling
- Designing deductive databases
	P. Helman, R. Veroff
- A tableau-based theorem prover
	F. Oppacher, E. Suen
- Basic research problems:
    The problem of finding a strategy to control binary paramodulation
	L. Wos
- Errata:
    A. Yahya and L.J. Henschen: Deduction in non-Horn databases, J.
    Automated reasoning 1 (1985) 141-160
    W.McCune and L. Wos: A case study in automated theorem proving:
    finding sages in combinatory logic, J. Automated reasoning 3 (1987)
    91-107
- Books received
- Announcements

			CONTENTS VOLUME 3 (1987)

Articles:
- A note on a canonical theory with undecidable unification and matching
  problem
	A. Bockmayr
- A method for the mechanical derivation of formulas in elementary
  geometry
	S.-C. Chou
- A more expressive formulation of many sorted logic
	A.G. Cohn
- Unification in Abelian semigroups
	A. Herold, J.H. Siekmann
- Explicit representation of terms defined by counter examples
	J.-L. Lassez, K. Marriott
- How to clear a block: a theory of plans
	Z. Manna, R. Waldinger
- Link inheritance in abstract clause graphs
	H.J. Ohlbach
- Adding equality to semantic tableaux
	S.V. Reeves
- Obvious inferences
	P. Rudnicki
- A comparison of the variable-abstraction and constant-abstraction methods
  for associative-commutative unification
	M.E. Stickel
- Choosing directions for rules
	R. Treitel, M.R. Genesereth
- Hierarchical deduction
	T.-C. Wang, W.W. Bledsoe

Basic research problems:
- Some obstacles to the automation of reasoning, and the problem of
  redundant information
	L. Wos
- The problem of choosing the inference rule to employ
	L. Wos
- The problem of definition expansion and contraction
	L. Wos
- The problem of extending the set of support strategy
	L. Wos

Problem corner:
- A case study in automated theorem proving: finding sages in combinatory
  logic
	W. McCune, L. Wos
- Proving self-utterances
	M. Miller, D. Perlis
- Some experiments in nonassociative ring theory with an automated theorem
  prover
	R.L. Stevens
- Case studies of Z-module reasoning: proving benchmark theorems from ring
  theory
	T.-C. Wang

- Announcements
- Change of address
- Editor's note


			CONTENTS VOLUME 2

ISSUE 4, December 1986

- Editorial announcement
- Automated reasoning in geometry theorem proving with prolog
	H. Coelho, L.M. Pereiro
- A class of confluent term rewriting systems and unification
	J.-H. You, P.A. Subrahmanyam
- Problem corner:
    A foray into combinatory logic
	B. Glickfeld
- Announcement
- Change of address
- Author index
- Subject index

ISSUE 3, september 1986

- Editor's preface to Basic principles of mechanical theorem proving in
  elementary geometries by Wu Wen-tsun
	J. Strother Moore
- Basic principles of mechanical theorem proving in elementary geometries
	W. Wen-Tsun
- Proving geometry theorems with rewrite rules
	S.-C. Chou, W.F. Schelter
- Editor's note
	J.H. Siekmann
- Unification under associativity and idempotence is of type nullary
	M. Schmidt-Schauss
- The theory of idempotent semigroups is of unification type zero
	F. Baader
- Problem corner:
    Set theory in first-order logic: Clauses for G”del's axioms
	R. Boyer, E. Lusk, W. McCune, R. Overbeek, M. Stickel, L. Wos

ISSUE 2, 1986

- Correctness criteria of some algorithms for uncertain reasoning using
  incidence calculus
	A. Bundy
- Automated analysis of operators on state tables: A technique for
  intelligent search
	T. Kramer
- Negation as failure. Completeness of the query evaluation process for
  horn clause programs with recursive definitions
	C. Aquilano, R. Barbuti, P. Bocchetti, M. Martelli
- A decision procedure for combinations of propositional temporal logic
  and other specialized theories
	D.A. Plaisted
- Problem corner:
    Seventy-five problems for testing automatic theorem provers
	F.J. Pelletier
- Call for papers

ISSUE 1, 1986

- Job-shop scheduling using automated reasoning: A case study of the
  car-sequencing problem
	B.D. Parrello, W.C. Kabat, L. Wos
- Intelligent backtracing in deduction systems by means of extended
  unification graphs
	W. Dilger, A. Janson
- Proving termination of normalization functions for conditional expressions
	L.C. Paulson
- Unification in datastructure multisets
	W. Bttner
- Problem corner:
    Schubert's steamroller problem: Formulations and solutions
	M.E. Stickel
- Announcement
- Addresses of editor-in-chief and editorial board


		CONTENTS VOLUME 1

ISSUE 4, 1985

- Automated deduction by theory resolution
	M.E. Stickel
- Robot selection expert "Rose"
	J.G. Mauceri
- Circumspection and implicit definability
	J. Doyle
- Towards mechanical metamathematics
	N. Shankar

Problem corner:
- Predicate logic hacker tricks
	H.J. Ohlbach

- Changes of address
- Author index
- Subject index

ISSUE 3, 1985

- Experiments with semantic paramodulation
	W. McCune, L. Henschen
- Incidence calculus: a mechanism for probabilistic reasoning
	A. Bundy
- Writing programs that construct proofs
	R.L. Constable, T.B. Knoblock, J.L. Bates

Problem corner:
- The lion and the unicorn
	H.J. Ohlbach, M. Schmidt-Schauss

ISSUE 2, 1985

- An experiment with the Boyer-Moore theorem prover: a proof of Wilson's
  theorem
	D.M. Russinoff
- Deduction in non-horn databases
	A. Yahya, L.J. Henschen
- The concept and implementation of skeletal plans
	P.E. Friedland, Y. Iwasaki

Problem corner:
- Reasoning about equality
	E.L. Lusk, R.A. Overbeek

- Announcements
- Changes of address

ISSUE 1, 1985

- Editorial: a journal is born
	L. Wos

An overview of automated reasoning and related fields:
  What is automated reasoning?
	L. Wos
  Logic programming
	F. Pereira
  Research in intelligent robots
	R. Hong
  Program verification
	R.S. Boyer, J. Strother Moore
  What is automated theorem proving?
	W.W. Bledsoe, L.J. Henschen
  Expert systems
	B.G. Buchanan
  Nonclassical logic theorem proving
	G. Wrightson
  What is program synthesis?
	C. Green
  References

- A knowledge-based system for acquiring the conceptual structure of a
  diagnostic expert system
	J.S. Bennett, Roget
- On the role of automated theorem proving in the compile-time derivation
  of concurrency
	C. Lengauer
- Non-horn problems
	E. Lusk, R. Overbeek
- Information for authors
- Addresses of editor-in-chief and editorial board