LEADER 06345nam 22005535 450 001 996465940003316 005 20200630174056.0 010 $a3-540-39861-9 024 7 $a10.1007/3-540-16780-3 035 $a(CKB)1000000000230543 035 $a(SSID)ssj0000320753 035 $a(PQKBManifestationID)11264086 035 $a(PQKBTitleCode)TC0000320753 035 $a(PQKBWorkID)10259111 035 $a(PQKB)11582402 035 $a(DE-He213)978-3-540-39861-5 035 $a(PPN)155210688 035 $a(EXLCZ)991000000000230543 100 $a20121227d1986 u| 0 101 0 $aeng 135 $aurnn|008mamaa 181 $ctxt 182 $cc 183 $acr 200 10$a8th International Conference on Automated Deduction$b[electronic resource] $eOxford, England, July 27- August 1, 1986. Proceedings /$fedited by Jörg H. Siekmann 205 $a1st ed. 1986. 210 1$aBerlin, Heidelberg :$cSpringer Berlin Heidelberg :$cImprint: Springer,$d1986. 215 $a1 online resource (XII, 716 p.) 225 1 $aLecture Notes in Computer Science,$x0302-9743 ;$v230 300 $aBibliographic Level Mode of Issuance: Monograph 311 $a3-540-16780-3 327 $aConnections 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. 410 0$aLecture Notes in Computer Science,$x0302-9743 ;$v230 606 $aMathematical logic 606 $aArtificial intelligence 606 $aMathematical Logic and Foundations$3https://scigraph.springernature.com/ontologies/product-market-codes/M24005 606 $aMathematical Logic and Formal Languages$3https://scigraph.springernature.com/ontologies/product-market-codes/I16048 606 $aArtificial Intelligence$3https://scigraph.springernature.com/ontologies/product-market-codes/I21000 615 0$aMathematical logic. 615 0$aArtificial intelligence. 615 14$aMathematical Logic and Foundations. 615 24$aMathematical Logic and Formal Languages. 615 24$aArtificial Intelligence. 676 $a511.3 702 $aSiekmann$b Jörg H$4edt$4http://id.loc.gov/vocabulary/relators/edt 906 $aBOOK 912 $a996465940003316 996 $a8th International Conference on Automated Deduction$92831112 997 $aUNISA