9th International Conference on Automated Deduction

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 forsituations.- 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.