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

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.

---

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.

---

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.
Content:
Front Matter....Pages -
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

---

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.
Content:
Front Matter....Pages -
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
....