| Document Type
|
:
|
BL
|
| Record Number
|
:
|
746048
|
| Doc. No
|
:
|
b565997
|
| Main Entry
|
:
|
edited by Jörg H. Siekmann.
|
| Title & Author
|
:
|
8th International Conference on Automated Deduction : : Oxford, England, July 27-August 1, 1986 : proceedings\ edited by Jörg H. Siekmann.
|
| Publication Statement
|
:
|
Berlin ; New York : Springer-Verlag, ©1986.
|
| Series Statement
|
:
|
Lecture notes in computer science, 230.
|
| Page. NO
|
:
|
(ix, 708 pages) : illustrations
|
| ISBN
|
:
|
3540398619
|
|
|
:
|
: 9783540398615
|
| Contents
|
:
|
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.
|
| Subject
|
:
|
Automatic theorem proving -- Congresses.
|
| Subject
|
:
|
Automatic theorem proving.
|
| Subject
|
:
|
Logic, Symbolic and mathematical -- Congresses.
|
| Added Entry
|
:
|
Jörg H Siekmann
|
| Parallel Title
|
:
|
Eighth International Conference on Automated Deduction
|