| |
|
|
|
|
|
|
|
|
1. |
Record Nr. |
UNISA996465940003316 |
|
|
Titolo |
8th International Conference on Automated Deduction [[electronic resource] ] : Oxford, England, July 27- August 1, 1986. Proceedings / / edited by Jörg H. Siekmann |
|
|
|
|
|
|
|
Pubbl/distr/stampa |
|
|
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1986 |
|
|
|
|
|
|
|
|
|
ISBN |
|
|
|
|
|
|
Edizione |
[1st ed. 1986.] |
|
|
|
|
|
Descrizione fisica |
|
1 online resource (XII, 716 p.) |
|
|
|
|
|
|
Collana |
|
Lecture Notes in Computer Science, , 0302-9743 ; ; 230 |
|
|
|
|
|
|
Disciplina |
|
|
|
|
|
|
Soggetti |
|
Mathematical logic |
Artificial intelligence |
Mathematical Logic and Foundations |
Mathematical Logic and Formal Languages |
Artificial Intelligence |
|
|
|
|
|
|
|
|
Lingua di pubblicazione |
|
|
|
|
|
|
Formato |
Materiale a stampa |
|
|
|
|
|
Livello bibliografico |
Monografia |
|
|
|
|
|
Note generali |
|
Bibliographic Level Mode of Issuance: Monograph |
|
|
|
|
|
|
Nota di contenuto |
|
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. |
|
|
|
|
|
| |