## 10th International Conference on Automated Deduction: Kaiserslautern, FRG, July 24-27, 1990. ProceedingsThis 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. |

### What people are saying - Write a review

We haven't found any reviews in the usual places.

### Contents

Keynote Address | 1 |

Session | 5 |

The Theorem Prover of the Program Verifier Tatzelwurm | 6 |

Session | 9 |

Session | 13 |

A Complete Semantic Back Chaining Proof System | 16 |

0 | 38 |

A HighPerformance Parallel Theorem Prover | 40 |

Presenting Intuitive Deductions via Symmetric Simplification | 336 |

Toward Mechanical Methods for Streamlining Proofs | 351 |

Ordered Rewriting and Confluence | 366 |

Complete Sets of Reductions with Constraints | 381 |

Rewrite Systems for Varieties of Semigroups | 396 |

Improving Associative Path Orderings | 411 |

Invited Talk | 426 |

Simultaneous Paramodulation | 442 |

Substitutionbased Compilation of Extended Rules in Deductive Databases | 57 |

Theory and Implementation | 72 |

An Abstraction of Definite Horn Programs | 87 |

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 Strjvebased Subset Prover | 193 |

RittWus Decomposition Algorithm and Geometry Theorem Proving | 207 |

Encoding a DependentType ACalculus 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 |

Hyper Resolution and Equality Axioms without Function Substitutions | 456 |

Session 12 | 470 |

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 |

William McCune | 663 |

677 | |

AProlog | 682 |

### Common terms and phrases

aABq ajaq ajnj algorithm aouis aq UBD aqi ui asnBp auios Automated Theorem Proving C-equation C-term case-free clause contrapositives Definition equations example first-order logic formula Horn clauses iBqi implementation induction conclusion induction hypothesis inductive proof inference interpretation jBqj JJIM jooad jooid joojd Lemma literal Logic Programming mega-clauses metavariables model elimination Moqs nodes NQTHM paraconsistent logics paramodulation pasn pire pjnoM plus(y processor Prolog proof tree proving punojS punoq q;iM q^iM qjiM qoiqM qons quantified recursive rewrite rippling-out sajnj saop semantics siqi siqj Skolem function SLDNF strategy subgoals substitution rule suija SUIOIXB Suisn theorem prover uaAiS uaaq uaqM uiojj UIQJJ uoipas uoipnpap uoipunj uuoj variables wave front wave rules XBUI Xjuo