E-Books durchsuchen

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<InlineEquation ID="IE1"> <InlineMediaObject> <ImageObject Color="BlackWhite" FileRef="558_3540528857_Chapter_14_TeX2GIFIE1.gif" Format="GIF" Rendition="HTML" Type="Linedraw" /> </InlineMediaObject><EquationSource Format="TEX">$$\subseteq$$</EquationSource> </InlineEquation>: 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 <Emphasis Type="Italic">E</Emphasis>-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 <Emphasis Type="Italic">E</Emphasis>-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 O<Superscript>Y</Superscript>S<Superscript>T</Superscript>ER-CL<Superscript>A</Superscript>M 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 <Emphasis Type="Italic">Tatzelwurm</Emphasis>

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 equational unification

Tutorial on λProlog

Tutorial on compilation techniques for logics

Tutorial on high-performance theorem provers: Efficient implementation and parallelisation

Tutorial on program-synthetic deduction

Tutorial on rewrite-based theorem proving

Tutorial on computing models of propositional logics