10th International Conference on Automated Deduction: Kaiserslautern, FRG, July 24-27, 1990. Proceedings

Front Cover
Mark E. Stickel
Springer Science & Business Media, Jul 17, 1990 - Computers - 688 pages
0 Reviews
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.
 

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
LISSThe Logic Inference Search System
677
AProlog
682
Copyright

Common terms and phrases