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

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