10th International Conference on Automated Deduction

A theorem prover for a computational logic.- A complete semantic back chaining proof system.- Parallelizing the closure computation in automated deduction.- Partheo: A high-performance parallel theorem prover.- Substitution-based compilation of extended rules in deductive databases.- Automatic theorem proving in paraconsistent logics: Theory and implementation.- Case-free programs: An abstraction of definite horn programs.- Generalized well-founded semantics for logic programs.- Tactical theorem proving in program verification.- Extensions to the rippling-out tactic for guiding inductive proofs.- Guiding induction proofs.- Term rewriting induction.- A resolution principle for clauses with constraints.- Str+ve $$\subseteq$$ : The Str+ve-based subset prover.- Ritt-Wu's decomposition algorithm and geometry theorem proving.- Encoding a dependent-type ?-calculus in a logic programming language.- Investigations into proof-search in a system of first-order dependent function types.- Equality of terms containing associative-commutative functions and commutative binding operators is isomorphism complete.- An improved general E-unification method.- Some results on equational unification.- Unification in a combination of equational theories: an efficient algorithm.- SLIM: An automated reasoner for equivalences, applied to set theory.- An examination of the prolog technology theorem-prover.- Presenting intuitive deductions via symmetric simplification.- Toward mechanical methods for streamlining proofs.- Ordered rewriting and confluence.- Complete sets of reductions with constraints.- Rewrite systems for varieties of semigroups.- Improving associative path orderings.- Perspectives on automated deduction.- On restrictions of ordered paramodulation with simplification.- Simultaneous paramodulation.- Hyper resolution and equality axioms without function substitutions.- Automatic acquisition of search guiding heuristics.- Automated reasoning contributes to mathematics and logic.-