عنوان

8th International Conference on Automated Deduction :

شابک

3540398619

شابک

9783540398615

شماره

b565997

عنوان اصلي

8th International Conference on Automated Deduction :

نام عام مواد

[Book]

ساير اطلاعات عنواني

Oxford, England, July 27-August 1, 1986 : proceedings

نام نخستين پديدآور

edited by Jörg H. Siekmann.

محل نشرو پخش و غیره

Berlin ; New York

نام ناشر، پخش کننده و غيره

Springer-Verlag

تاریخ نشرو بخش و غیره

©1986.

نام خاص و کميت اثر

(ix, 708 pages) : illustrations

عنوان فروست

Lecture notes in computer science, 230.

متن يادداشت

Connections and higher-order logic --; Commutation, transformation, and termination --; Full-commutation and fair-termination in equational (and combined) term-rewriting systems --; An actual implementation of a procedure that mechanically proves termination of rewriting systems based on inequalities between polynomial interpretations --; Proving termination of associative commutative rewriting systems by rewriting --; Relating resolution and algebraic completion for Horn logic --; A simple non-termination test for the Knuth-Bendix method --; A new formula for the execution of categorical combinators --; Proof by induction using test sets --; How to prove equivalence of term rewriting systems without induction --; Sufficient completeness, term rewriting systems and "anti-unification" --; A new method for establishing refutational completeness in theorem proving --; A theory of diagnosis from first principles --; Some contributions to the logical analysis of circumscription --; Modal theorem proving --; Computational aspects of three-valued logic --; Resolution and quantified epistemic logics --; A commonsense theory of nonmonotonic reasoning --; Negative paramodulation --; The heuristics and experimental results of a new hyperparamodulation: HL-resolution --; ECR: An equality conditional resolution proof procedure --; Using narrowing to do isolation in symbolic equation solving --; an experiment in automated reasoning --; Formulation of induction formulas in verification of prolog programs --; Program verifier "Tatzelwurm": Reasoning about systems systems of linear inequalities --; An interactive verification system based on dynamic logic --; What you always wanted to know about clause graph resolution --; Parallel theorem proving with connection graphs --; Theory links in semantic graphs --; Abstraction using generalization functions --; An improvement of deduction plans: Refutation plans --; Controlling deduction with proof condensation and heuristics --; Nested resolution --; Mechanizing constructive proofs --; Implementing number theory: An experiment with Nuprl --; Parallel algorithms for term matching --; Unification in combinations of collapse-free theories with disjoint sets of function symbols --; Combination of unification algorithms --; Unification in the data structure sets --; NP-completeness of the set unification and matching problems --; Matching with distributivity --; Unification in boolean rings --; Some relationships between unification, restricted unification, and matching --; A classification of many-sorted unification problems --; Unification in many-sorted equational theories --; Classes of first order formulas under various satisfiability definitions --; Diamond formulas in the dynamic logic of recursively enumerable programs --; A prolog machine --; A prolog technology theorem prover: Implementation by an extended prolog compiler --; Paths to high-performance automated theorem proving --; Purely functional implementation of a logic --; Causes for events: Their computation and applications --; How to clear a block: Plan formation in situational logic --; Deductive synthesis of sorting programs --; The TPS theorem proving system --; Trspec: A term rewriting based system for algebraic specifications --; Highly parallel inference machine --; Automatic theorem proving in the ISDV system --; The karlsruhe induction theorem proving system --; Overview of a theorem-prover for a computational logic --; GEO-prover --; A geometry theorem prover developed at UT --; The markgraf karl refutation procedure (MKRP) --; The J-machine: Functional programming with combinators --; The illinois prover: A general purpose resolution theorem prover --; Theorem proving systems of the Formel project --; The passau RAP system: Prototyping algebraic specifications using conditional narrowing --; RRL: A rewrite rule laboratory --; A geometry theorem prover based on Buchberger's algorithm --; REVE a rewrite rule laboratory --; ITP at argonne national laboratory --; Autologic at university of victoria --; Thinker --; The KLAUS automated deduction system --; The KRIPKE automated theorem proving system --; SHD-prover at university of texas at austin.

عنوان اصلي به زبان ديگر

Eighth International Conference on Automated Deduction

موضوع مستند نشده

Automatic theorem proving -- Congresses.

موضوع مستند نشده

Automatic theorem proving.

موضوع مستند نشده

Logic, Symbolic and mathematical -- Congresses.

مستند نام اشخاص تاييد نشده

edited by Jörg H. Siekmann.

مستند نام اشخاص تاييد نشده

Jörg H Siekmann

نام الکترونيکي

نوع ماده

[Book]

تكميل شده

Y