10th International Conference on Automated Deduction: Kaiserslautern, FRG, July 24-27, 1990. ProceedingsMark E. Stickel "This volume contains the papers presented at the 10th International Conference on Automated Deduction (CADE-10). CADE is the major forum at which research on all aspects of automated deduction is presented. Although automated deduction research is also presented at more general artificial intelligence conferences, the CADE conferences have no peer in the concentration and quality of their contributions to this topic. The papers included range from theory to implementation and experimentation, from propositional to higher-order calculi and nonclassical logics; they refine and use a wealth of methods including resolution, paramodulation, rewriting, completion, unification and induction; and they work with a variety of applications including program verification, logic programming, deductive databases, and theorem proving in many domains. The volume also contains abstracts of 20 implementations of automated deduction systems. The authors of about half the papers are from the United States, many are from Western Europe, and many too are from the rest of the world. The proceedings of the 5th, 6th, 7th, 8th and 9th CADE conferences are published as Volumes 87, 138, 170, 230, 310 in the series Lecture Notes in Computer Science."--PUBLISHER'S WEBSITE. |
Contents
Keynote Address | 4 |
Session | 13 |
Session 5 | 16 |
A Complete Semantic Back Chaining Proof System | 22 |
A HighPerformance Parallel Theorem Prover | 46 |
Substitutionbased Compilation of Extended Rules in Deductive Databases | 63 |
Theory and Implementation | 78 |
An Abstraction of Definite Horn Programs | 87 |
Ordered Rewriting and Confluence | 366 |
Complete Sets of Reductions with Constraints | 381 |
Rewrite Systems for Varieties of Semigroups | 396 |
Improving Associative Path Orderings | 411 |
Joachim Steinbach | 425 |
Simultaneous Paramodulation | 442 |
Hyper Resolution and Equality Axioms without Function Substitutions | 456 |
Automatic Acquisition of Search Guiding Heuristics | 470 |
Generalized Wellfounded Semantics for Logic Programs | 102 |
Tactical Theorem Proving in Program Verification | 117 |
Extensions to the RipplingOut Tactic for Guiding Inductive Proofs | 132 |
Guiding Induction Proofs | 147 |
Term Rewriting Induction | 162 |
A Resolution Principle for Clauses with Constraints | 178 |
The Str+vebased Subset Prover | 193 |
RittWus Decomposition Algorithm and Geometry Theorem Proving | 207 |
Encoding a DependentType XCalculus in a Logic Programming Language | 221 |
Investigations into ProofSearch in a System of FirstOrder Dependent | 236 |
Equality of Terms Containing AssociativeCommutative Functions | 251 |
Some Results on Equational Unification | 276 |
an Efficient Algorithm | 292 |
An Automated Reasoner for Equivalences Applied to Set Theory | 308 |
An Examination of the Prolog Technology TheoremProver | 322 |
Presenting Intuitive Deductions via Symmetric Simplification | 336 |
Toward Mechanical Methods for Streamlining Proofs | 351 |
Automated Reasoning Contributes to Mathematics and Logic | 485 |
A Mechanically Assisted Constructive Proof in Category Theory | 500 |
Dynamic Logic as a Uniform Framework for Theorem Proving in Intensional Logic | 514 |
A TableauxBased Theorem Prover for a Decidable Subset of Default Logic | 528 |
Computing Prime Implicants | 543 |
Minimizing the Number of Clauses by Renaming | 558 |
Session 14 | 573 |
Programming by Example and Proving by Example Using Higherorder Unification | 588 |
Retrieving Library Identifiers via Equational Matching of Types | 603 |
Unification in Monoidal Theories | 618 |
Invited Talk | 633 |
The OysterClam System | 647 |
The Romulus Proof Checker | 651 |
A Dissolutionbased Theorem Prover | 665 |
The Abstract Clause Engine | 679 |
Amy Felty Elsa Gunter Dale Miller Frank Pfenning | 682 |
Other editions - View all
Proceedings: 10th International Conference on Automated Deduction ... Mark E. Stickel No preview available - 1990 |
Common terms and phrases
Abstract algorithm applied atoms Automated Reasoning Automated Theorem Proving axioms C-equation C-term C₁ calculus case-free closure complete Computer Science constraint contains context critical pairs d₁ decomposition defined Definition denote derivation disjunctive E-unification empty example finite first-order first-order logic formula function symbols ground instance Herbrand heuristics Horn clauses implementation induction conclusion induction hypothesis inductive proof inference rules instantiation interpretation joinable Lemma literal Logic Programming mega-clauses metavariables method minimal model elimination multiset natural deduction negation nodes Normal Form NQTHM occur pair paraconsistent logics paramodulation plus(y predicate problem processor Prolog proof tree Proposition PTTP quantifiers query recursive resolution restricted quantifiers restriction result rewriting system rippling-out RQ-clauses S₁ semantics sequence Skolem function step strategy subgoals subset substitution rule subterm Suppose t₁ term rewriting term rewriting system theorem proving unifiable unification universally quantified variables wave front wave rules well-founded well-typed