9th International Conference on Automated Deduction: Argonne, Illinois, USA, May 23–26, 1988 Proceedings

First-order theorem proving using conditional rewrite rules....Pages 1-20
Elements of Z-module reasoning....Pages 21-40
Learning and applying generalised solutions using higher order resolution....Pages 41-60
Specifying theorem provers in a higher-order logic programming language....Pages 61-80
Query processing in quantitative logic programming....Pages 81-100
An environment for automated reasoning about partial functions....Pages 101-110
The use of explicit plans to guide inductive proofs....Pages 111-120
Logicalc: An environment for interactive proof development....Pages 121-130
Implementing verification strategies in the KIV-system....Pages 131-140
Checking natural language proofs....Pages 141-150
Consistency of rule-based expert systems....Pages 151-161
A mechanizable induction principle for equational specifications....Pages 162-181
Finding canonical rewriting systems equivalent to a finite set of ground equations in polynomial time....Pages 182-196
Towards efficient "knowledge-based" automated theorem proving for non-standard logics....Pages 197-217
Propositional temporal interval logic is PSPACE complete....Pages 218-237
Computational metatheory in Nuprl....Pages 238-257
Type inference in Prolog....Pages 258-277
Procedural interpretation of non-horn logic programs....Pages 278-293
Recursive query answering with non-horn clauses....Pages 294-312
Case inference in resolution-based languages....Pages 313-322
Notes on Prolog program transformations, Prolog style, and efficient compilation to the Warren abstract machine....Pages 323-332
Exploitation of parallelism in prototypical deduction problems....Pages 333-343
A decision procedure for unquantified formulas of graph theory....Pages 344-357
Adventures in associative-commutative unification (A summary)....Pages 358-367
Unification in finite algebras is unitary(?)....Pages 368-377
Unification in a combination of arbitrary disjoint equational theories....Pages 378-396
Partial unification for graph based equational reasoning....Pages 397-414
SATCHMO: A theorem prover implemented in Prolog....Pages 415-434
Term rewriting: Some experimental results....Pages 435-453
Analogical reasoning and proof discovery....Pages 454-468
Hyper-chaining and knowledge-based theorem proving....Pages 469-486
Linear modal deductions....Pages 487-499
A resolution calculus for modal logics....Pages 500-516
Solving disequations in equational theories....Pages 517-526
On word problems in Horn theories....Pages 527-537
Canonical conditional rewrite systems....Pages 538-549
Program synthesis by completion with dependent subtypes....Pages 550-562
Reasoning about systems of linear inequalities....Pages 563-572
A subsumption algorithm based on characteristic matrices....Pages 573-581
A restriction of factoring in binary resolution....Pages 582-591
Supposition-based logic for automated nonmonotonic reasoning....Pages 592-601
Argument-bounded algorithms as a basis for automated termination proofs....Pages 602-621
Two automated methods in implementation proofs....Pages 622-642
A new approach to universal unfication and its application to AC-unification....Pages 643-657
An implementation of a dissolution-based system employing theory links....Pages 658-674
Decision procedure for autoepistemic logic....Pages 675-684
Logical matrix generation and testing....Pages 685-693
Optimal time bounds for parallel term matching....Pages 694-703
Challenge equality problems in lattice theory....Pages 704-709
Single axioms in the implicational propositional calculus....Pages 710-713
Challenge problems focusing on equality and combinatory logic: Evaluating automated theorem-proving programs....Pages 714-729
Challenge problems from nonassociative rings for theorem provers....Pages 730-734
An interactive enhancement to the Boyer-Moore theorem prover....Pages 735-736
A goal directed theorem prover....Pages 737-737
m-NEVER system summary....Pages 738-739
EFS — An interactive Environment for Formal Systems....Pages 740-741
Ontic: A knowledge representation system for mathematics....Pages 742-743
Some tools for an inference laboratory (ATINF)....Pages 744-745
Quantlog: A system for approximate reasoning in inconsistent formal systems....Pages 746-747
LP: The larch prover....Pages 748-749
The KLAUS automated deduction system....Pages 750-751
A Prolog technology theorem prover....Pages 752-753
λProlog: An extended logic programming language....Pages 754-755
SYMEVAL: A theorem prover based on the experimental logic....Pages 756-757
ZPLAN: An automatic reasoning system for situations....Pages 758-759
The TPS theorem proving system....Pages 760-761
MOLOG: A modal PROLOG....Pages 762-763
PARTHENON: A parallel theorem prover for non-horn clauses....Pages 764-765
An nH-Prolog implementation....Pages 766-767
RRL: A rewrite rule laboratory....Pages 768-769
Geometer: A theorem prover for algebraic geometry....Pages 770-771
Isabelle: The next seven hundred theorem provers....Pages 772-773
The CHIP system : Constraint handling in Prolog....Pages 774-775