%A Allen Goldberg %T Average case complexity of the satisfiability problem %J Proceedings of the 4th Workshop on Automated Deduction %C Austin, Texas %D February 1979 %K cade cade4 %P 1-6 %A Steve Winker %T Generation and verification of finite models and counterexamples using an automated theorem prover answering two open questions %J Proceedings of the 4th Workshop on Automated Deduction %C Austin, Texas %D February 1979 %K cade cade4 %P 7-13 %A Mabry Tyson %A W.W. Bledsoe %T Conflicting bindings and generalized substitutions %J Proceedings of the 4th Workshop on Automated Deduction %C Austin, Texas %D February 1979 %K cade cade4 %P 14-18 %A Peter B. Andrews %T General matings %J Proceedings of the 4th Workshop on Automated Deduction %C Austin, Texas %D February 1979 %K cade cade4 %P 19-25 %A Drew McDermott %A Jon Doyle %T Non-monotonic logic I %J Proceedings of the 4th Workshop on Automated Deduction %C Austin, Texas %D February 1979 %K cade cade4 %P 26-35 %A Daniel Brand %A John A. Darringer %A William H. Joyner,\ Jr. %T Completeness of conditional reduction %J Proceedings of the 4th Workshop on Automated Deduction %C Austin, Texas %D February 1979 %K cade cade4 %P 36-42 %A Vincent J. Digricoli %T Resolution by unification and equality %J Proceedings of the 4th Workshop on Automated Deduction %C Austin, Texas %D February 1979 %K cade cade4 %P 43-52 %A Hans Bucken %T Reduction systems and small cancellation theory %J Proceedings of the 4th Workshop on Automated Deduction %C Austin, Texas %D February 1979 %K cade cade4 %P 53-59 %A Robert Elliot Filman %T Observation and inference applied in a formal representation system %J Proceedings of the 4th Workshop on Automated Deduction %C Austin, Texas %D February 1979 %K cade cade4 %P 60-66 %A Derek C. Oppen %T Complexity of combinations of quantifier-free theories %J Proceedings of the 4th Workshop on Automated Deduction %C Austin, Texas %D February 1979 %K cade cade4 %P 67-72 %A Avra Cohn %T High level proof in LCF %J Proceedings of the 4th Workshop on Automated Deduction %C Austin, Texas %D February 1979 %K cade cade4 %P 73-80 %A Robert E. Shostak %T Deciding linear inequalities by computing loop residues %J Proceedings of the 4th Workshop on Automated Deduction %C Austin, Texas %D February 1979 %K cade cade4 %P 81-89 %A John Doyle %T A glimpse of truth maintenance %J Proceedings of the 4th Workshop on Automated Deduction %C Austin, Texas %D February 1979 %K cade cade4 %P 90-96 %A Howard Elliot Shrobe %T Explicit control of reasoning in the programmer's apprentice %J Proceedings of the 4th Workshop on Automated Deduction %C Austin, Texas %D February 1979 %K cade cade4 %P 97-102 %A Sharon Sickel %T Invertibility of logic programs %J Proceedings of the 4th Workshop on Automated Deduction %C Austin, Texas %D February 1979 %K cade cade4 %P 103-109 %A Dennis de\ Champeaux %T Sub-problem finder and instance checker - two cooperating processors for theorem provers %J Proceedings of the 4th Workshop on Automated Deduction %C Austin, Texas %D February 1979 %K cade cade4 %P 110-114 %A Philip Klahr %T Partial proofs and partial answers %J Proceedings of the 4th Workshop on Automated Deduction %C Austin, Texas %D February 1979 %K cade cade4 %P 115-121 %A Philip T. Cox %T Representation economy in a mechanical theorem-prover %J Proceedings of the 4th Workshop on Automated Deduction %C Austin, Texas %D February 1979 %K cade cade4 %P 122-128 %A Zohar Manna %T A deductive approach to program synthesis %J Proceedings of the 4th Workshop on Automated Deduction %C Austin, Texas %D February 1979 %K cade cade4 %P 129-139 %A Wolfgang Bibel %T Syntax-directed, semantics-supported program synthesis %J Proceedings of the 4th Workshop on Automated Deduction %C Austin, Texas %D February 1979 %K cade cade4 %P 140-147 %A Graham Wrightson %T A proof procedure for higher-order modal logic %J Proceedings of the 4th Workshop on Automated Deduction %C Austin, Texas %D February 1979 %K cade cade4 %P 148-154 %A Frank Brown %T A theorem prover for meta-theory %J Proceedings of the 4th Workshop on Automated Deduction %C Austin, Texas %D February 1979 %K cade cade4 %P 155-160 %A Michael J. Fay %T First-order unification in an equational theory %J Proceedings of the 4th Workshop on Automated Deduction %C Austin, Texas %D February 1979 %K cade cade4 %P 161-167 %A D.S. Lankford %A A.M. Ballantyne %T The refutation completeness of blocked permutative narrowing and resolution %J Proceedings of the 4th Workshop on Automated Deduction %C Austin, Texas %D February 1979 %K cade cade4 %P 168-174 %A M. Livesay %A J. Siekmann %A P. Szabo %A E. Unvericht %T Unification problems for combinations of associativity, commutativity, distributivity and idempotence axioms %J Proceedings of the 4th Workshop on Automated Deduction %C Austin, Texas %D February 1979 %K cade cade4 %P 175-184 %A Luigia Aiello %A Richard W. Weyhrauch %T Using meta-theoretic reasoning to do algebra %J Proceedings of the 5th Conference on Automated Deduction %C Les Arcs, France %D 1980 %O published as Lecture Notes in Computer Science 87 %K cade cade5 %P 1-13 %A Gabor Belovari %A J.A. Campbell %T Generating contours of integration: an application of Prolog in symbolic computing %J Proceedings of the 5th Conference on Automated Deduction %C Les Arcs, France %D 1980 %O published as Lecture Notes in Computer Science 87 %K cade cade5 %P 14-23 %A Alan Bundy %A Bob Welham %T Using meta-level inference for selective application of multiple rewrite rules in algebraic manipulation %J Proceedings of the 5th Conference on Automated Deduction %C Les Arcs, France %D 1980 %O published as Lecture Notes in Computer Science 87 %K cade cade5 %P 24-38 %A C.A. Goad %T Proofs as descriptions of computation %J Proceedings of the 5th Conference on Automated Deduction %C Les Arcs, France %D 1980 %O published as Lecture Notes in Computer Science 87 %K cade cade5 %P 39-52 %A Gerard Guiho %A Christian Gresse %T Program synthesis from incomplete specifications %J Proceedings of the 5th Conference on Automated Deduction %C Les Arcs, France %D 1980 %O published as Lecture Notes in Computer Science 87 %K cade cade5 %P 53-62 %A Laurent Kott %T A system for proving equivalences of recursive programs %J Proceedings of the 5th Conference on Automated Deduction %C Les Arcs, France %D 1980 %O published as Lecture Notes in Computer Science 87 %K cade cade5 %P 63-69 %A W.W. Bledsoe %A Larry M. Hines %T Variable elimination and chaining in a resolution-based prover for inequalities %J Proceedings of the 5th Conference on Automated Deduction %C Les Arcs, France %D 1980 %O published as Lecture Notes in Computer Science 87 %K cade cade5 %P 70-87 %A A. Ferro %A E.G. Omodeo %A J.T. Schwartz %T Decision procedures for some fragments of set theory %J Proceedings of the 5th Conference on Automated Deduction %C Les Arcs, France %D 1980 %O published as Lecture Notes in Computer Science 87 %K cade cade5 %P 88-96 %A D.W. Loveland %A R.E. Shostak %T Simplifying interpreted formulas %J Proceedings of the 5th Conference on Automated Deduction %C Les Arcs, France %D 1980 %O published as Lecture Notes in Computer Science 87 %K cade cade5 %P 97-109 %A Frederick C. Furtek %T Specification and verification of real-time distributed systems using the theory of constraints %J Proceedings of the 5th Conference on Automated Deduction %C Les Arcs, France %D 1980 %O published as Lecture Notes in Computer Science 87 %K cade cade5 %P 110-125 %A Leonard Friedman %T Reasoning by plausible inference %J Proceedings of the 5th Conference on Automated Deduction %C Les Arcs, France %D 1980 %O published as Lecture Notes in Computer Science 87 %K cade cade5 %P 126-142 %A Alan M. Thompson %T Logical support in a time-varying model %J Proceedings of the 5th Conference on Automated Deduction %C Les Arcs, France %D 1980 %O published as Lecture Notes in Computer Science 87 %K cade cade5 %P 143-153 %A Paul Y. Gloess %T An experiment with the Boyer-Moore theorem prover: a proof of the correctness of a simple parser of expressions %J Proceedings of the 5th Conference on Automated Deduction %C Les Arcs, France %D 1980 %O published as Lecture Notes in Computer Science 87 %K cade cade5 %P 154-169 %A Jacek Leszczylowski %T An experiment with "Edinburgh LCF" %J Proceedings of the 5th Conference on Automated Deduction %C Les Arcs, France %D 1980 %O published as Lecture Notes in Computer Science 87 %K cade cade5 %P 170-181 %A R.P. Nederpelt %T An approach to theorem proving on the basis of a typed lambda-calculus %J Proceedings of the 5th Conference on Automated Deduction %C Les Arcs, France %D 1980 %O published as Lecture Notes in Computer Science 87 %K cade cade5 %P 182-194 %A Paul Y. Gloess %A Jean-Pierre H. Laurent %T Adding dynamic paramodulation to rewrite algorithms %J Proceedings of the 5th Conference on Automated Deduction %C Les Arcs, France %D 1980 %O published as Lecture Notes in Computer Science 87 %K cade cade5 %P 195-207 %K Knuth-Bendix %A L. Wos %A R. Overbeek %A L. Henschen %T Hyperparamodulation: a refinement of paramodulation %J Proceedings of the 5th Conference on Automated Deduction %C Les Arcs, France %D 1980 %O published as Lecture Notes in Computer Science 87 %K cade cade5 %P 208-219 %A Roddy W. Erickson %A David R. Musser %T The AFFIRM theorem prover: proof forests and management of large proofs %J Proceedings of the 5th Conference on Automated Deduction %C Les Arcs, France %D 1980 %O published as Lecture Notes in Computer Science 87 %K cade cade5 %P 220-231 %A Ross A. Overbeek %A Ewing L. Lusk %T Data structures and control architecture for implementation of theorem-proving programs %J Proceedings of the 5th Conference on Automated Deduction %C Les Arcs, France %D 1980 %O published as Lecture Notes in Computer Science 87 %K cade cade5 %P 232-249 %A Helga Noll %T A note on resolution: how to get rid of factoring without loosing completeness %J Proceedings of the 5th Conference on Automated Deduction %C Les Arcs, France %D 1980 %O published as Lecture Notes in Computer Science 87 %K cade cade5 %P 250-263 %A D.A. Plaisted %T Abstraction mappings in mechanical theorem proving %J Proceedings of the 5th Conference on Automated Deduction %C Les Arcs, France %D 1980 %O published as Lecture Notes in Computer Science 87 %K cade cade5 %P 264-280 %A Peter B. Andrews %T Transforming matings into natural deduction proofs %J Proceedings of the 5th Conference on Automated Deduction %C Les Arcs, France %D 1980 %O published as Lecture Notes in Computer Science 87 %K cade cade5 %P 281-292 %A Maurice Bruynooghe %T Analysis of dependencies to improve the behaviour of logic programs %J Proceedings of the 5th Conference on Automated Deduction %C Les Arcs, France %D 1980 %O published as Lecture Notes in Computer Science 87 %K cade cade5 %P 293-305 %K control, backtracking, conflict resolution %A Luis Moniz Pereira %A Antonio Porto %T Selective backtracking for logic programs %J Proceedings of the 5th Conference on Automated Deduction %C Les Arcs, France %D 1980 %O published as Lecture Notes in Computer Science 87 %K cade cade5 %P 306-317 %A Jean-Marie Hullot %T Canonical forms and unification %J Proceedings of the 5th Conference on Automated Deduction %C Les Arcs, France %D 1980 %O published as Lecture Notes in Computer Science 87 %K cade cade5 %P 318-334 %A Hans-Josef Jeanrond %T Deciding unique termination of permutative rewriting systems: choose your term algebra carefully %J Proceedings of the 5th Conference on Automated Deduction %C Les Arcs, France %D 1980 %O published as Lecture Notes in Computer Science 87 %K cade cade5 %P 335-355 %A J.A. Goguen %T How to prove algebraic inductive hypotheses without induction %J Proceedings of the 5th Conference on Automated Deduction %C Les Arcs, France %D 1980 %O published as Lecture Notes in Computer Science 87 %K cade cade5 %P 356-373 %A P.T. Cox %A T. Pietrzykowski %T A complete, nonredundant algorithm for reversed Skolemization %J Proceedings of the 5th Conference on Automated Deduction %C Les Arcs, France %D 1980 %O published as Lecture Notes in Computer Science 87 %K cade cade5 %P 374-385 %A L. Wos %T Solving open questions with an automated theorem-proving program %J Proceedings of the 6th Conference on Automated Deduction %C New York, USA %D June 1982 %O published as Lecture Notes in Computer Science 138 %K cade cade6 %P 1-31 %A R.E. Shostak %A Richard Schwartz %A P.M. Melliar-Smith %T STP: a mechanized logic for specification and verification %J Proceedings of the 6th Conference on Automated Deduction %C New York, USA %D June 1982 %O published as Lecture Notes in Computer Science 138 %K cade cade6 %P 32-49 %A Dale A. Miller %A Eve Longini Cohen %A Peter B. Andrews %T A look at TPS %J Proceedings of the 6th Conference on Automated Deduction %C New York, USA %D June 1982 %O published as Lecture Notes in Computer Science 138 %K cade cade6 %P 50-69 %A Ewing L. Lusk %A William W. McCune %A Ross A. Overbeek %T Logic machine architecture: kernel functions %J Proceedings of the 6th Conference on Automated Deduction %C New York, USA %D June 1982 %O published as Lecture Notes in Computer Science 138 %K cade cade6 %P 70-84 %A Ewing L. Lusk %A William W. McCune %A Ross A. Overbeek %T Logic machine architecture: inference mechanisms %J Proceedings of the 6th Conference on Automated Deduction %C New York, USA %D June 1982 %O published as Lecture Notes in Computer Science 138 %K cade cade6 %P 85-108 %A S.K. Winker %A L. Wos %T Procedure implementation through demodulation and related tricks %J Proceedings of the 6th Conference on Automated Deduction %C New York, USA %D June 1982 %O published as Lecture Notes in Computer Science 138 %K cade cade6 %P 109-131 %A Bernard Silver %T The application of homogenization to simultaneous equations %J Proceedings of the 6th Conference on Automated Deduction %C New York, USA %D June 1982 %O published as Lecture Notes in Computer Science 138 %K cade cade6 %P 132-143 %A Leon Sterling %A Alan Bundy %T Meta-level inference and program verification %J Proceedings of the 6th Conference on Automated Deduction %C New York, USA %D June 1982 %O published as Lecture Notes in Computer Science 138 %K cade cade6 %P 144-150 %A Richard W. Weyhrauch %T An example of FOL using metatheory: formalizing reasoning systems and introducing derived inference rules %J Proceedings of the 6th Conference on Automated Deduction %C New York, USA %D June 1982 %O published as Lecture Notes in Computer Science 138 %K cade cade6 %P 151-158 %A S. Greenbaum %A A. Nagasaka %A P. O'Rourke %A D. Plaisted %T Comparison of natural deduction and locking resolution implementations %J Proceedings of the 6th Conference on Automated Deduction %C New York, USA %D June 1982 %O published as Lecture Notes in Computer Science 138 %K cade cade6 %P 159-171 %A Douglas R. Smith %T Derived preconditions and their use in program synthesis %J Proceedings of the 6th Conference on Automated Deduction %C New York, USA %D June 1982 %O published as Lecture Notes in Computer Science 138 %K cade cade6 %P 172-193 %A Chris Goad %T Automatic construction of special purpose programs %J Proceedings of the 6th Conference on Automated Deduction %C New York, USA %D June 1982 %O published as Lecture Notes in Computer Science 138 %K cade cade6 %P 194-208 %A Robert E. Shostak %T Deciding combinations of theories %J Proceedings of the 6th Conference on Automated Deduction %C New York, USA %D June 1982 %O published as Lecture Notes in Computer Science 138 %K cade cade6 %P 209-222 %A Tomasz Pietrzykowsky %A Stanislaw Matwin %T Exponential improvement of efficient backtracking: a strategy for plan-based deduction %J Proceedings of the 6th Conference on Automated Deduction %C New York, USA %D June 1982 %O published as Lecture Notes in Computer Science 138 %K cade cade6 %P 223-239 %A Stanislaw Matwin %A Tomasz Pietrzykowsky %T Exponential improvement of exhaustive backtracking: data structure and implementation %J Proceedings of the 6th Conference on Automated Deduction %C New York, USA %D June 1982 %O published as Lecture Notes in Computer Science 138 %K cade cade6 %P 240-259 %A Dov M. Gabbay %T Intuitionistic basis for non-monotonic logic %J Proceedings of the 6th Conference on Automated Deduction %C New York, USA %D June 1982 %O published as Lecture Notes in Computer Science 138 %K cade cade6 %P 260-273 %A Alan M. Frisch %A James F. Allen %T Knowledge retrieval as limited inference %J Proceedings of the 6th Conference on Automated Deduction %C New York, USA %D June 1982 %O published as Lecture Notes in Computer Science 138 %K cade cade6 %P 274-291 %A Jack Minker %T On indefinite databases and the closed world assumption %J Proceedings of the 6th Conference on Automated Deduction %C New York, USA %D June 1982 %O published as Lecture Notes in Computer Science 138 %K cade cade6 %P 292-308 %A Ricardo Caffera %T Proof by matrix reduction as plan + validation %J Proceedings of the 6th Conference on Automated Deduction %C New York, USA %D June 1982 %O published as Lecture Notes in Computer Science 138 %K cade cade6 %P 309-325 %A K.M. Hornig %A W. Bibel %T Improvements of a tautology-testing algorithm %J Proceedings of the 6th Conference on Automated Deduction %C New York, USA %D June 1982 %O published as Lecture Notes in Computer Science 138 %K cade cade6 %P 326-341 %A Lawrence J. Henschen %A Shamim A. Naqvi %T Representing infinite sequences of resolvents in recursive first-order Horn databases %J Proceedings of the 6th Conference on Automated Deduction %C New York, USA %D June 1982 %O published as Lecture Notes in Computer Science 138 %K cade cade6 %P 342-359 %A Ronald V. Book %T The power of the Church-Rosser property for string rewriting systems %J Proceedings of the 6th Conference on Automated Deduction %C New York, USA %D June 1982 %O published as Lecture Notes in Computer Science 138 %K cade cade6 %P 360-368 %A J. Siekmann %A P. Szabo %T Universal unification and a classification of equational theories %J Proceedings of the 6th Conference on Automated Deduction %C New York, USA %D June 1982 %O published as Lecture Notes in Computer Science 138 %K cade cade6 %P 369-389 %A Jorg H. Siekmann %T Universal unification %J Proceedings of the 7th Conference on Automated Deduction %C Napa, California %D May 1984 %O published as Lecture Notes in Computer Science 170 %K cade cade7 %P 1-42 %A Ewing L. Lusk %A Ross A. Overbeek %T A portable environment for research in automated reasoning %J Proceedings of the 7th Conference on Automated Deduction %C Napa, California %D May 1984 %O published as Lecture Notes in Computer Science 170 %K cade cade7 %P 43-52 %A Deepak Kapur %A Balakrishnan Krishnamurthy %T A natural proof system based on rewriting techniques %J Proceedings of the 7th Conference on Automated Deduction %C Napa, California %D May 1984 %O published as Lecture Notes in Computer Science 170 %K cade cade7 %P 53-64 %A Jussi Ketonen %T EKL - a mathematically oriented proof checker %J Proceedings of the 7th Conference on Automated Deduction %C Napa, California %D May 1984 %O published as Lecture Notes in Computer Science 170 %K cade cade7 %P 65-79 %A Silvio Ursic %T A linear characterization of NP-complete problems %J Proceedings of the 7th Conference on Automated Deduction %C Napa, California %D May 1984 %O published as Lecture Notes in Computer Science 170 %K cade cade7 %P 80-100 %A Allen van\ Gelder %T A satisfiability tester for non-clausal propositional calculus %J Proceedings of the 7th Conference on Automated Deduction %C Napa, California %D May 1984 %O published as Lecture Notes in Computer Science 170 %K cade cade7 %P 101-112 %A Ana R. Cavalli %A Luis Farinas del\ Cerro %T A decision method for linear temporal logic %J Proceedings of the 7th Conference on Automated Deduction %C Napa, California %D May 1984 %O published as Lecture Notes in Computer Science 170 %K cade cade7 %P 113-127 %A D. Lankford %A G. Butler %A A. Ballantyne %T A progress report on new decision algorithms for finitely presented Abelian groups %J Proceedings of the 7th Conference on Automated Deduction %C Napa, California %D May 1984 %O published as Lecture Notes in Computer Science 170 %K cade cade7 %P 128-141 %A Philippe le\ Chenadec %T Canonical forms in finitely presented algebras %J Proceedings of the 7th Conference on Automated Deduction %C Napa, California %D May 1984 %O published as Lecture Notes in Computer Science 170 %K cade cade7 %P 142-165 %A Pierre Lescanne %T Term rewriting systems and algebra %J Proceedings of the 7th Conference on Automated Deduction %C Napa, California %D May 1984 %O published as Lecture Notes in Computer Science 170 %K cade cade7 %P 166-174 %A Jean-Pierre Jouannaud %A Miguel Munoz %T Termination of a set of rules modula a set of equations %J Proceedings of the 7th Conference on Automated Deduction %C Napa, California %D May 1984 %O published as Lecture Notes in Computer Science 170 %K cade cade7 %P 175-193 %A Francois Fages %T Associative-commutative unification %J Proceedings of the 7th Conference on Automated Deduction %C Napa, California %D May 1984 %O published as Lecture Notes in Computer Science 170 %K cade cade7 %P 194-208 %A Donald Simon %T A linear time algorithm for a subcase of second order instantiation %J Proceedings of the 7th Conference on Automated Deduction %C Napa, California %D May 1984 %O published as Lecture Notes in Computer Science 170 %K cade cade7 %P 209-223 %A Claude Kirchner %T A new equational unification method: a generalisation of Martelli-Montanari's algorithm %J Proceedings of the 7th Conference on Automated Deduction %C Napa, California %D May 1984 %O published as Lecture Notes in Computer Science 170 %K cade cade7 %P 224-247 %A Mark E. Stickel %T A case study of theorem proving by the Knuth-Bendix method: discovering that x^3 = x implies ring commutativity %J Proceedings of the 7th Conference on Automated Deduction %C Napa, California %D May 1984 %O published as Lecture Notes in Computer Science 170 %K cade cade7 %P 248-258 %A L. Fribourg %T A narrowing procedure for theories with constructors %J Proceedings of the 7th Conference on Automated Deduction %C Napa, California %D May 1984 %O published as Lecture Notes in Computer Science 170 %K cade cade7 %P 259-281 %A Helene Kirchner %T A general inductive completion algorithm and application to abstract data types %J Proceedings of the 7th Conference on Automated Deduction %C Napa, California %D May 1984 %O published as Lecture Notes in Computer Science 170 %K cade cade7 %P 282-302 %A Patrick Suppes %T The next generation of interactive theorem provers %J Proceedings of the 7th Conference on Automated Deduction %C Napa, California %D May 1984 %O published as Lecture Notes in Computer Science 170 %K cade cade7 %P 303-315 %A L. Wos %A R. Veroff %A B. Smith %A W. McCune %T The linked inference principle, II: the user's viewpoint %J Proceedings of the 7th Conference on Automated Deduction %C Napa, California %D May 1984 %O published as Lecture Notes in Computer Science 170 %K cade cade7 %P 316-332 %A Etienne Paul %T A new interpretation of the resolution principle %J Proceedings of the 7th Conference on Automated Deduction %C Napa, California %D May 1984 %O published as Lecture Notes in Computer Science 170 %K cade cade7 %P 333-355 %A David A. Plaisted %T Using examples, case analysis, and dependency graphs in theorem proving %J Proceedings of the 7th Conference on Automated Deduction %C Napa, California %D May 1984 %O published as Lecture Notes in Computer Science 170 %K cade cade7 %P 356-374 %A Dale A. Miller %T Expansion tree proofs and their conversion to natural deduction proofs %J Proceedings of the 7th Conference on Automated Deduction %C Napa, California %D May 1984 %O published as Lecture Notes in Computer Science 170 %K cade cade7 %P 375-393 %A Frank Pfenning %T Analytic and non-analytic proofs %J Proceedings of the 7th Conference on Automated Deduction %C Napa, California %D May 1984 %O published as Lecture Notes in Computer Science 170 %K cade cade7 %P 394-413 %A Jack Minker %A Donald Perlis %T Applications of protected circumscription %J Proceedings of the 7th Conference on Automated Deduction %C Napa, California %D May 1984 %O published as Lecture Notes in Computer Science 170 %K cade cade7 %P 414-425 %A Kenneth Forsythe %A Stanislaw Matwin %T Implementation strategies for plan-based deduction %J Proceedings of the 7th Conference on Automated Deduction %C Napa, California %D May 1984 %O published as Lecture Notes in Computer Science 170 %K cade cade7 %P 426-444 %A David A. Schmidt %T A programming notation for tactical reasoning %J Proceedings of the 7th Conference on Automated Deduction %C Napa, California %D May 1984 %O published as Lecture Notes in Computer Science 170 %K cade cade7 %P 445-459 %A Ketan Mulmuley %T The mechanization of existence proofs of recursive predicates %J Proceedings of the 7th Conference on Automated Deduction %C Napa, California %D May 1984 %O published as Lecture Notes in Computer Science 170 %K cade cade7 %P 460-475 %A Alex Pelin %A Jean H. Gallier %T Solving word problems in free algebras using complexity functions %J Proceedings of the 7th Conference on Automated Deduction %C Napa, California %D May 1984 %O published as Lecture Notes in Computer Science 170 %K cade cade7 %P 476-495 %A Hans-Jurgen Ohlbach %A Graham Wrightson %T Solving a problem in relevance logic with an automated theorem prover %J Proceedings of the 7th Conference on Automated Deduction %C Napa, California %D May 1984 %O published as Lecture Notes in Computer Science 170 %K cade cade7 %P 496-508 %A Peter B. Andrews %T Connections and higher-order logic %J Proceedings of the 8th Conference on Automated Deduction %C Oxford, England %D July 1986 %O published as Lecture Notes in Computer Science 230 %K cade cade8 %P 1-4 %A Leo Bachmair %A Nachum Dershowitz %T Commutation, transformation, and termination %J Proceedings of the 8th Conference on Automated Deduction %C Oxford, England %D July 1986 %O published as Lecture Notes in Computer Science 230 %K cade cade8 %P 5-20 %A Sara Porat %A Nissim Francez %T Full-commutation and fair-termination in equational (and combined) term-rewriting systems %J Proceedings of the 8th Conference on Automated Deduction %C Oxford, England %D July 1986 %O published as Lecture Notes in Computer Science 230 %K cade cade8 %P 21-41 %A Ahlem Ben Cherifs %A Pierre Lescanne %T An actual implementation of a procedure that mechanically proves termination of rewriting systems based on inequalities between polynomial interpretations %J Proceedings of the 8th Conference on Automated Deduction %C Oxford, England %D July 1986 %O published as Lecture Notes in Computer Science 230 %K cade cade8 %P 42-51 %A Isabelle Gnaedig %A Pierre Lescanne %T Proving termination of associative commutative rewriting systems by rewriting %J Proceedings of the 8th Conference on Automated Deduction %C Oxford, England %D July 1986 %O published as Lecture Notes in Computer Science 230 %K cade cade8 %P 52-61 %A Roland Dietrich %T Relating resolution and algebraic completion for Horn logic %J Proceedings of the 8th Conference on Automated Deduction %C Oxford, England %D July 1986 %O published as Lecture Notes in Computer Science 230 %K cade cade8 %P 62-76 %A David A. Plaisted %T A simple non-termination test for the Knuth-Bendix method %J Proceedings of the 8th Conference on Automated Deduction %C Oxford, England %D July 1986 %O published as Lecture Notes in Computer Science 230 %K cade cade8 %P 77-88 %A R.D. Lins %T A new formula for the execution of categorical combinators %J Proceedings of the 8th Conference on Automated Deduction %C Oxford, England %D July 1986 %O published as Lecture Notes in Computer Science 230 %K cade cade8 %P 89-98 %A Deepak Kapur %A Paliath Narendran %A Hantao Zhang %T Proof by induction using test sets %J Proceedings of the 8th Conference on Automated Deduction %C Oxford, England %D July 1986 %O published as Lecture Notes in Computer Science 230 %K cade cade8 %P 99-117 %A Yoshihito Toyama %T How to prove equivalence of term rewriting systems without induction %J Proceedings of the 8th Conference on Automated Deduction %C Oxford, England %D July 1986 %O published as Lecture Notes in Computer Science 230 %K cade cade8 %P 118-127 %A Hubert Comon %T Sufficient completeness, term rewriting systems and "anti-unification" %J Proceedings of the 8th Conference on Automated Deduction %C Oxford, England %D July 1986 %O published as Lecture Notes in Computer Science 230 %K cade cade8 %P 128-140 %A Jieh Hsiang %A Michael Rusinowitch %T A new method for establishing refutational completeness in theorem proving %J Proceedings of the 8th Conference on Automated Deduction %C Oxford, England %D July 1986 %O published as Lecture Notes in Computer Science 230 %K cade cade8 %P 141-152 %A Gerhard Jaeger %T Some contributions to the logical analysis of circumscription %J Proceedings of the 8th Conference on Automated Deduction %C Oxford, England %D July 1986 %O published as Lecture Notes in Computer Science 230 %K cade cade8 %P 154-171 %A Martin Abadi %A Zohar Manna %T Modal theorem proving %J Proceedings of the 8th Conference on Automated Deduction %C Oxford, England %D July 1986 %O published as Lecture Notes in Computer Science 230 %K cade cade8 %P 172-189 %A P.H. Schmitt %T Computational aspects of three-valued logic %J Proceedings of the 8th Conference on Automated Deduction %C Oxford, England %D July 1986 %O published as Lecture Notes in Computer Science 230 %K cade cade8 %P 190-198 %A Kurt Konolidge %T Resolution and quantified epistemic logics %J Proceedings of the 8th Conference on Automated Deduction %C Oxford, England %D July 1986 %O published as Lecture Notes in Computer Science 230 %K cade cade8 %P 199-208 %A Frank M. Brown %T A commonsense theory of nonmonotonic reasoning %J Proceedings of the 8th Conference on Automated Deduction %C Oxford, England %D July 1986 %O published as Lecture Notes in Computer Science 230 %K cade cade8 %P 209-226 %A L. Wos %A W. McCune %T Negative paramodulation %J Proceedings of the 8th Conference on Automated Deduction %C Oxford, England %D July 1986 %O published as Lecture Notes in Computer Science 230 %K cade cade8 %P 227-239 %A Younghwan Lim %T The heuristics and experimental results of a new hyperparamodulation: HL-resolution %J Proceedings of the 8th Conference on Automated Deduction %C Oxford, England %D July 1986 %O published as Lecture Notes in Computer Science 230 %K cade cade8 %P 240-253 %A Tie Cheng Wang %T ECR: an equality conditional resolution proof procedure %J Proceedings of the 8th Conference on Automated Deduction %C Oxford, England %D July 1986 %O published as Lecture Notes in Computer Science 230 %K cade cade8 %P 254-271 %A A.J.J. Dick %A R.J. Cunningham %T Using narrowing to do isolation in symbolic equation solving %J Proceedings of the 8th Conference on Automated Deduction %C Oxford, England %D July 1986 %O published as Lecture Notes in Computer Science 230 %K cade cade8 %P 272-280 %A Tadashi Kanamori %A Hiroshi Fujita %T Formulation of induction formulas in verification of Prolog programs %J Proceedings of the 8th Conference on Automated Deduction %C Oxford, England %D July 1986 %O published as Lecture Notes in Computer Science 230 %K cade cade8 %P 281-299 %A Thomas Kaufl %T Program verifier "Tatzelwurm": reasoning about systems of linear inequalities %J Proceedings of the 8th Conference on Automated Deduction %C Oxford, England %D July 1986 %O published as Lecture Notes in Computer Science 230 %K cade cade8 %P 300-305 %A R. Hahnle %A M. Heisel %A W. Reif %A W. Stephan %T An interactive verification system based on dynamic logic %J Proceedings of the 8th Conference on Automated Deduction %C Oxford, England %D July 1986 %O published as Lecture Notes in Computer Science 230 %K cade cade8 %P 306-315 %A Norbert Eisinger %T What you always wanted to know about clause graph resolution %J Proceedings of the 8th Conference on Automated Deduction %C Oxford, England %D July 1986 %O published as Lecture Notes in Computer Science 230 %K cade cade8 %P 316-336 %A Rasiah Loganantharaj %A Robert A. Mueller %T Parallel theorem proving with connection graphs %J Proceedings of the 8th Conference on Automated Deduction %C Oxford, England %D July 1986 %O published as Lecture Notes in Computer Science 230 %K cade cade8 %P 337-352 %A Neil V. Murray %A Erik Rosenthal %T Theory links in semantic graphs %J Proceedings of the 8th Conference on Automated Deduction %C Oxford, England %D July 1986 %O published as Lecture Notes in Computer Science 230 %K cade cade8 %P 353-364 %A David A. Plaisted %T Abstraction using generalization functions %J Proceedings of the 8th Conference on Automated Deduction %C Oxford, England %D July 1986 %O published as Lecture Notes in Computer Science 230 %K cade cade8 %P 365-376 %A Hans-Albert Schneider %T An improvement of deduction plans: refutation plans %J Proceedings of the 8th Conference on Automated Deduction %C Oxford, England %D July 1986 %O published as Lecture Notes in Computer Science 230 %K cade cade8 %P 377-383 %A F. Oppacher %A E. Suen %T Controlling deduction with proof condensation and heuristics %J Proceedings of the 8th Conference on Automated Deduction %C Oxford, England %D July 1986 %O published as Lecture Notes in Computer Science 230 %K cade cade8 %P 384-393 %A Jonathan Traugott %T Nested resolution %J Proceedings of the 8th Conference on Automated Deduction %C Oxford, England %D July 1986 %O published as Lecture Notes in Computer Science 230 %K cade cade8 %P 394-402 %A Gerard Huet %T Mechanizing constructive proofs %J Proceedings of the 8th Conference on Automated Deduction %C Oxford, England %D July 1986 %O published as Lecture Notes in Computer Science 230 %K cade cade8 %P 403-415 %A Cynthia Dwork %A Paris Kanellakis %A Larry Stackmeyer %T Parallel algorithms for term matching %J Proceedings of the 8th Conference on Automated Deduction %C Oxford, England %D July 1986 %O published as Lecture Notes in Computer Science 230 %K cade cade8 %P 416-430 %A Erik Tiden %T Unification in combinations of collapse-free theories with disjoint sets of function symbols %J Proceedings of the 8th Conference on Automated Deduction %C Oxford, England %D July 1986 %O published as Lecture Notes in Computer Science 230 %K cade cade8 %P 431-449 %A Alexander Herold %T Combination of unification algorithms %J Proceedings of the 8th Conference on Automated Deduction %C Oxford, England %D July 1986 %O published as Lecture Notes in Computer Science 230 %K cade cade8 %P 450-469 %A Wolfram Buttner %T Unification in the data structure sets %J Proceedings of the 8th Conference on Automated Deduction %C Oxford, England %D July 1986 %O published as Lecture Notes in Computer Science 230 %K cade cade8 %P 470-488 %A Deepak Kapur %A Paliath Narendran %T NP-completeness of the set unification and matching problems %J Proceedings of the 8th Conference on Automated Deduction %C Oxford, England %D July 1986 %O published as Lecture Notes in Computer Science 230 %K cade cade8 %P 489-495 %A Jalel Mzali %T Matching with distributivity %J Proceedings of the 8th Conference on Automated Deduction %C Oxford, England %D July 1986 %O published as Lecture Notes in Computer Science 230 %K cade cade8 %P 496-505 %A Ursula Martin %A Tobias Nipkow %T Unification in boolean rings %J Proceedings of the 8th Conference on Automated Deduction %C Oxford, England %D July 1986 %O published as Lecture Notes in Computer Science 230 %K cade cade8 %P 506-513 %A Hans-Jurgen Burckert %T Some relationships between unification restricted unification, and matching %J Proceedings of the 8th Conference on Automated Deduction %C Oxford, England %D July 1986 %O published as Lecture Notes in Computer Science 230 %K cade cade8 %P 514-524 %A Christoph Walther %T A classification of many-sorted unification problems %J Proceedings of the 8th Conference on Automated Deduction %C Oxford, England %D July 1986 %O published as Lecture Notes in Computer Science 230 %K cade cade8 %P 525-537 %A Manfred Schmidt-Schauss %T Unification in many-sorted equational theories %J Proceedings of the 8th Conference on Automated Deduction %C Oxford, England %D July 1986 %O published as Lecture Notes in Computer Science 230 %K cade cade8 %P 538-552 %A H. Kleine Buning %A Th. Lettmann %T Classes of first-order formulas under various satisfiabilities definitions %J Proceedings of the 8th Conference on Automated Deduction %C Oxford, England %D July 1986 %O published as Lecture Notes in Computer Science 230 %K cade cade8 %P 553-563 %A Volker Weispfenning %T Diamond formulas in the dynamic logic of recursively enumerable programs %J Proceedings of the 8th Conference on Automated Deduction %C Oxford, England %D July 1986 %O published as Lecture Notes in Computer Science 230 %K cade cade8 %P 564-571 %A Mark E. Stickel %T A Prolog technology theorem prover: implementation by an extended Prolog compiler %J Proceedings of the 8th Conference on Automated Deduction %C Oxford, England %D July 1986 %O published as Lecture Notes in Computer Science 230 %K cade cade8 %P 572-587 %A Ralph Butler %A Ewing Lusk %A William McCune %A Ross Overbeek %T Paths to high-performance automated theorem proving %J Proceedings of the 8th Conference on Automated Deduction %C Oxford, England %D July 1986 %O published as Lecture Notes in Computer Science 230 %K cade cade8 %P 588-597 %A F.K. Hanna %A N. Daeche %T Purely functional implementation of a logic %J Proceedings of the 8th Conference on Automated Deduction %C Oxford, England %D July 1986 %O published as Lecture Notes in Computer Science 230 %K cade cade8 %P 598-607 %A P.T. Cox %A T. Pietrzykowski %T Causes for events: their computation and applications %J Proceedings of the 8th Conference on Automated Deduction %C Oxford, England %D July 1986 %O published as Lecture Notes in Computer Science 230 %K cade cade8 %P 608-621 %A Zohar Manna %A Richard Waldinger %T How to clear a block: plan formation in situational logic %J Proceedings of the 8th Conference on Automated Deduction %C Oxford, England %D July 1986 %O published as Lecture Notes in Computer Science 230 %K cade cade8 %P 622-640 %A Jonathan Traugott %T Deductive synthesis of sorting programs %J Proceedings of the 8th Conference on Automated Deduction %C Oxford, England %D July 1986 %O published as Lecture Notes in Computer Science 230 %K cade cade8 %P 641-660 %A Peter B. Andrews %A Frank Pfenning %A Sunil Issar %A C.P. Klapper %T The TPS theorem proving system (extended abstract) %J Proceedings of the 8th Conference on Automated Deduction %C Oxford, England %D July 1986 %O published as Lecture Notes in Computer Science 230 %K cade cade8 %P 663-664 %A J. Avenhaus %A B. Bennington %A R. Gobel %A K. Madlener %T TRSPEC: a term rewriting based system for algebraic specifications (extended abstract) %J Proceedings of the 8th Conference on Automated Deduction %C Oxford, England %D July 1986 %O published as Lecture Notes in Computer Science 230 %K cade cade8 %P 665-667 %A M. Bayerl %T Highly parallel inference machine (extended abstract) %J Proceedings of the 8th Conference on Automated Deduction %C Oxford, England %D July 1986 %O published as Lecture Notes in Computer Science 230 %K cade cade8 %P 668-669 %A Christoph Beierle %A Walter Olthoff %A Angelika Voss %T Automatic theorem proving in the ISDV system (extended abstract) %J Proceedings of the 8th Conference on Automated Deduction %C Oxford, England %D July 1986 %O published as Lecture Notes in Computer Science 230 %K cade cade8 %P 670-671 %A S. Biundo %A B. Hummel %A D. Hutter %A C. Walther %T The Karlsruhe induction theorem proving system (extended abstract) %J Proceedings of the 8th Conference on Automated Deduction %C Oxford, England %D July 1986 %O published as Lecture Notes in Computer Science 230 %K cade cade8 %P 672-674 %A Robert S. Boyer %A J. Strother Moore %T Overview of a theorem-prover for a computational logic (extended abstract) %J Proceedings of the 8th Conference on Automated Deduction %C Oxford, England %D July 1986 %O published as Lecture Notes in Computer Science 230 %K cade cade8 %P 675-678 %A Shang-Ching Chou %T GEO-prover - a geometry theorem prover developed at UT (extended abstract) %J Proceedings of the 8th Conference on Automated Deduction %C Oxford, England %D July 1986 %O published as Lecture Notes in Computer Science 230 %K cade cade8 %P 679-680 %A N. Eisinger %A H.J. Ohlbach %T The Markgraf Karl refutation procedure (MKRP) (extended abstract) %J Proceedings of the 8th Conference on Automated Deduction %C Oxford, England %D July 1986 %O published as Lecture Notes in Computer Science 230 %K cade cade8 %P 681-682 %A Jacek Gibert %T The J-machine: functional programming with combinators (extended abstract) %J Proceedings of the 8th Conference on Automated Deduction %C Oxford, England %D July 1986 %O published as Lecture Notes in Computer Science 230 %K cade cade8 %P 683-684 %A Steven Greenbaum %A David A. Plaisted %T The Illinois prover: a general purpose resolution theorem prover (extended abstract) %J Proceedings of the 8th Conference on Automated Deduction %C Oxford, England %D July 1986 %O published as Lecture Notes in Computer Science 230 %K cade cade8 %P 685-686 %A Gerard Huet %T Theorem proving systems of the Formel project8 (extended abstract) %J Proceedings of the 8th Conference on Automated Deduction %C Oxford, England %D July 1986 %O published as Lecture Notes in Computer Science 230 %K cade cade8 %P 687-688 %A Heinrich Hussmann %T The Passau RAP system: prototyping algebraic specifications using conditional narrowing (extended abstract) %J Proceedings of the 8th Conference on Automated Deduction %C Oxford, England %D July 1986 %O published as Lecture Notes in Computer Science 230 %K cade cade8 %P 689-690 %A Deepak Kapur %A G. Sivakumar %A Hantao Zhang %T RRL: a rewrite rule laboratory (extended abstract) %J Proceedings of the 8th Conference on Automated Deduction %C Oxford, England %D July 1986 %O published as Lecture Notes in Computer Science 230 %K cade cade8 %P 691-692 %A B. Kutzler %A S. Stifter %T A geometry theorem prover based pn Buchberger's algorithm (extended abstract) %J Proceedings of the 8th Conference on Automated Deduction %C Oxford, England %D July 1986 %O published as Lecture Notes in Computer Science 230 %K cade cade8 %P 693-694 %A Pierre Lescanne %T REVE a rewrite rule laboratory (extended abstract) %J Proceedings of the 8th Conference on Automated Deduction %C Oxford, England %D July 1986 %O published as Lecture Notes in Computer Science 230 %K cade cade8 %P 695-696 %A Ewing Lusk %A William McCune %A Ross Overbeek %T ITP at Argonne National Laboratory (extended abstract) %J Proceedings of the 8th Conference on Automated Deduction %C Oxford, England %D July 1986 %O published as Lecture Notes in Computer Science 230 %K cade cade8 %P 697-698 %A Charles G. Morgan %T AUTOLOGIC at University of Victoria (extended abstract) %J Proceedings of the 8th Conference on Automated Deduction %C Oxford, England %D July 1986 %O published as Lecture Notes in Computer Science 230 %K cade cade8 %P 699-700 %A Francis Jeffry Pelletier %T THINKER (extended abstract) %J Proceedings of the 8th Conference on Automated Deduction %C Oxford, England %D July 1986 %O published as Lecture Notes in Computer Science 230 %K cade cade8 %P 701-702 %A Mark E. Stickel %T The KLAUS automated deduction system (extended abstract) %J Proceedings of the 8th Conference on Automated Deduction %C Oxford, England %D July 1986 %O published as Lecture Notes in Computer Science 230 %K cade cade8 %P 703-704 %A Paul B. Thistlewaite %A Michael A. McRobbie %A Robert K. Meyer %T The KRIPKE automated theorem proving system (extended abstract) %J Proceedings of the 8th Conference on Automated Deduction %C Oxford, England %D July 1986 %O published as Lecture Notes in Computer Science 230 %K cade cade8 %P 705-706 %A Tie Cheng Wang %T SHD-prover at University of Texas at Austin (extended abstract) %J Proceedings of the 8th Conference on Automated Deduction %C Oxford, England %D July 1986 %O published as Lecture Notes in Computer Science 230 %K cade cade8 %P 707-708