9th International Conference on Automated Deduction

This volume contains the papers presented at the Ninth International Conference on Automated Deduction (CADE-9) held May 23-26 at Argonne National Laboratory, Argonne, Illinois. The conference commemorates the twenty-fifth anniversary of the discovery of the resolution principle, which took place during the summer of 1963. The CADE conferences are a forum for reporting on research on all aspects of automated deduction, including theorem proving, logic programming, unification, deductive databases, term rewriting, ATP for non-standard logics, and program verification. All papers submitted to the conference were refereed by at least two referees, and the program committee accepted the 52 that appear here. Also included in this volume are abstracts of 21 implementations of automated deduction systems.

First-order theorem proving using conditional rewrite rules.- Elements of Z-module reasoning.- Learning and applying generalised solutions using higher order resolution.- Specifying theorem provers in a higher-order logic programming language.- Query processing in quantitative logic programming.- An environment for automated reasoning about partial functions.- The use of explicit plans to guide inductive proofs.- Logicalc: An environment for interactive proof development.- Implementing verification strategies in the KIV-system.- Checking natural language proofs.- Consistency of rule-based expert systems.- A mechanizable induction principle for equational specifications.- Finding canonical rewriting systems equivalent to a finite set of ground equations in polynomial time.- Towards efficient "knowledge-based" automated theorem proving for non-standard logics.- Propositional temporal interval logic is PSPACE complete.- Computational metatheory in Nuprl.- Type inference in Prolog.- Procedural interpretation of non-horn logic programs.- Recursive query answering with non-horn clauses.- Case inference in resolution-based languages.- Notes on Prolog program transformations, Prolog style, and efficient compilation to the Warren abstract machine.- Exploitation of parallelism in prototypical deduction problems.- A decision procedure for unquantified formulas of graph theory.- Adventures in associative-commutative unification (A summary).- Unification in finite algebras is unitary(?).- Unification in a combination of arbitrary disjoint equational theories.- Partial unification for graph based equational reasoning.- SATCHMO: A theorem prover implemented in Prolog.- Term rewriting: Some experimental results.- Analogical reasoning and proof discovery.- Hyper-chaining and knowledge-based theorem proving.- Linear modal deductions.- A resolution calculus for modal logics.- Solving disequations in equational theories.- On word problems in Horn theories.- Canonical conditional rewrite systems.- Program synthesis by completion with dependent subtypes.- Reasoning about systems of linear inequalities.- A subsumption algorithm based on characteristic matrices.- A restriction of factoring in binary resolution.- Supposition-based logic for automated nonmonotonic reasoning.- Argument-bounded algorithms as a basis for automated termination proofs.- Two automated methods in implementation proofs.- A new approach to universal unfication and its application to AC-unification.- An implementation of a dissolution-based system employing theory links.- Decision procedure for autoepistemic logic.- Logical matrix generation and testing.- Optimal time bounds for parallel term matching.- Challenge equality problems in lattice theory.- Single axioms in the implicational propositional calculus.- Challenge problems focusing on equality and combinatory logic: Evaluating automated theorem-proving programs.- Challenge problems from nonassociative rings for theorem provers.- An interactive enhancement to the Boyer-Moore theorem prover.- A goal directed theorem prover.- m-NEVER system summary.- EFS — An interactive Environment for Formal Systems.- Ontic: A knowledge representation system for mathematics.- Some tools for an inference laboratory (ATINF).- Quantlog: A system for approximate reasoning in inconsistent formal systems.- LP: The larch prover.- The KLAUS automated deduction system.- A Prolog technology theorem prover.- ?Prolog: An extended logic programming language.- SYMEVAL: A theorem prover based on the experimental logic.- ZPLAN: An automatic reasoning system for situations.- The TPS theorem proving system.- MOLOG: A modal PROLOG.- PARTHENON: A parallel theorem prover for non-horn clauses.- An nH-Prolog implementation.- RRL: A rewrite rule laboratory.- Geometer: A theorem prover for algebraic geometry.- Isabelle: The next seven hundred theorem provers.- The CHIP system : Constraint handling in Prolog.