内容

目次

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.- A mechanically assisted constructive proof in category theory.- Dynamic logic as a uniform framework for theorem proving in intensional logic.- A tableaux-based theorem prover for a decidable subset of default logic.- Computing prime implicants.- Minimizing the number of clauses by renaming.- Higher order E-unification.- Programming by example and proving by example using higher-order unification.- Retrieving library identifiers via equational matching of types.- Unification in monoidal theories.- A science of reasoning: Extended abstract.- The TPS theorem proving system.- Schemata.- Cylindric algebra equation solver.- The OYSTER-CLAM system.- A high-performance parallel theorem prover.- The romulus proof checker.- IMPS : An interactive mathematical proof system.- UNICOM: A refined completion based inductive theorem prover.- The theorem prover of the program verifier Tatzelwurm.- RCL: A lisp verification system.- Orme an implementation of completion procedures as sets of transitions rules.- Otter 2.0.- Dissolver: A dissolution-based theorem prover.- TRIP: An implementation of clausal rewriting.- OSCAR.- Expert thinker: An adaptation of F-Prolog to microcomputers.- A prolog technology theorem prover.- A general clause theorem prover.- Liss — The logic inference search system.- ACE: The abstract clause engine.- Tutorial on high-performance automated theorem proving.- Tutorial on reasoning and representation with concept languages.- Tutorial on ?Prolog.- Tutorial on equational unification.- Tutorial on compilation techniques for logics.- Tutorial on high-performance theorem provers: Efficient implementation and parallelisation.- Tutorial on rewrite-based theorem proving.- Tutorial on program-synthetic deduction.- Tutorial on computing models of propositional logics.