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.
Author(s): Robert S. Boyer, J Strother Moore (auth.), Mark E. Stickel (eds.)
Series: Lecture Notes in Computer Science 449
Edition: 1
Publisher: Springer-Verlag Berlin Heidelberg
Year: 1990
Language: English
Pages: 690
Tags: Artificial Intelligence (incl. Robotics); Mathematical Logic and Formal Languages
A theorem prover for a computational logic....Pages 1-15
A complete semantic back chaining proof system....Pages 16-27
Parallelizing the closure computation in automated deduction....Pages 28-39
Partheo: A high-performance parallel theorem prover....Pages 40-56
Substitution-based compilation of extended rules in deductive databases....Pages 57-71
Automatic theorem proving in paraconsistent logics: Theory and implementation....Pages 72-86
Case-free programs: An abstraction of definite horn programs....Pages 87-101
Generalized well-founded semantics for logic programs....Pages 102-116
Tactical theorem proving in program verification....Pages 117-131
Extensions to the rippling-out tactic for guiding inductive proofs....Pages 132-146
Guiding induction proofs....Pages 147-161
Term rewriting induction....Pages 162-177
A resolution principle for clauses with constraints....Pages 178-192
Str+ve $$\subseteq$$ : The Str+ve-based subset prover....Pages 193-206
Ritt-Wu's decomposition algorithm and geometry theorem proving....Pages 207-220
Encoding a dependent-type λ-calculus in a logic programming language....Pages 221-235
Investigations into proof-search in a system of first-order dependent function types....Pages 236-250
Equality of terms containing associative-commutative functions and commutative binding operators is isomorphism complete....Pages 251-260
An improved general E -unification method....Pages 261-275
Some results on equational unification....Pages 276-291
Unification in a combination of equational theories: an efficient algorithm....Pages 292-307
SLIM: An automated reasoner for equivalences, applied to set theory....Pages 308-321
An examination of the prolog technology theorem-prover....Pages 322-335
Presenting intuitive deductions via symmetric simplification....Pages 336-350
Toward mechanical methods for streamlining proofs....Pages 351-365
Ordered rewriting and confluence....Pages 366-380
Complete sets of reductions with constraints....Pages 381-395
Rewrite systems for varieties of semigroups....Pages 396-410
Improving associative path orderings....Pages 411-425
Perspectives on automated deduction....Pages 426-426
On restrictions of ordered paramodulation with simplification....Pages 427-441
Simultaneous paramodulation....Pages 442-455
Hyper resolution and equality axioms without function substitutions....Pages 456-469
Automatic acquisition of search guiding heuristics....Pages 470-484
Automated reasoning contributes to mathematics and logic....Pages 485-499
A mechanically assisted constructive proof in category theory....Pages 500-513
Dynamic logic as a uniform framework for theorem proving in intensional logic....Pages 514-527
A tableaux-based theorem prover for a decidable subset of default logic....Pages 528-542
Computing prime implicants....Pages 543-557
Minimizing the number of clauses by renaming....Pages 558-572
Higher order E -unification....Pages 573-587
Programming by example and proving by example using higher-order unification....Pages 588-602
Retrieving library identifiers via equational matching of types....Pages 603-617
Unification in monoidal theories....Pages 618-632
A science of reasoning: Extended abstract....Pages 633-640
The TPS theorem proving system....Pages 641-642
Schemata....Pages 643-644
Cylindric algebra equation solver....Pages 645-646
The O Y S T ER-CL A M system....Pages 647-648
A high-performance parallel theorem prover....Pages 649-650
The romulus proof checker....Pages 651-652
IMPS : An interactive mathematical proof system....Pages 653-654
UNICOM: A refined completion based inductive theorem prover....Pages 655-656
The theorem prover of the program verifier Tatzelwurm ....Pages 657-658
RCL: A lisp verification system....Pages 659-660
Orme an implementation of completion procedures as sets of transitions rules....Pages 661-662
Otter 2.0....Pages 663-664
Dissolver: A dissolution-based theorem prover....Pages 665-666
TRIP: An implementation of clausal rewriting....Pages 667-668
OSCAR....Pages 669-670
Expert thinker: An adaptation of F-Prolog to microcomputers....Pages 671-672
A prolog technology theorem prover....Pages 673-674
A general clause theorem prover....Pages 675-676
Liss — The logic inference search system....Pages 677-678
ACE: The abstract clause engine....Pages 679-680
Tutorial on high-performance automated theorem proving....Pages 681-681
Tutorial on reasoning and representation with concept languages....Pages 681-681
Tutorial on λProlog....Pages 682-682
Tutorial on equational unification....Pages 682-682
Tutorial on compilation techniques for logics....Pages 683-683
Tutorial on high-performance theorem provers: Efficient implementation and parallelisation....Pages 683-683
Tutorial on rewrite-based theorem proving....Pages 684-684
Tutorial on program-synthetic deduction....Pages 684-684
Tutorial on computing models of propositional logics....Pages 685-685
