<電子ブック>
8th International Conference on Automated Deduction : Oxford, England, July 27- August 1, 1986. Proceedings / edited by Jörg H. Siekmann
(Lecture Notes in Computer Science. ISSN:16113349 ; 230)
版 | 1st ed. 1986. |
---|---|
出版者 | (Berlin, Heidelberg : Springer Berlin Heidelberg : Imprint: Springer) |
出版年 | 1986 |
本文言語 | 英語 |
大きさ | XII, 716 p : online resource |
著者標目 | Siekmann, Jörg H editor SpringerLink (Online service) |
件 名 | LCSH:Mathematical logic LCSH:Machine theory LCSH:Artificial intelligence FREE:Mathematical Logic and Foundations FREE:Formal Languages and Automata Theory FREE:Artificial Intelligence |
一般注記 | 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 HTTP:URL=https://doi.org/10.1007/3-540-16780-3 |
目次/あらすじ
所蔵情報を非表示
電子ブック | 配架場所 | 資料種別 | 巻 次 | 請求記号 | 状 態 | 予約 | コメント | ISBN | 刷 年 | 利用注記 | 指定図書 | 登録番号 |
---|---|---|---|---|---|---|---|---|---|---|---|---|
電子ブック | オンライン | 電子ブック |
|
Springer eBooks | 9783540398615 |
|
電子リソース |
|
EB00224785 |
書誌詳細を非表示
データ種別 | 電子ブック |
---|---|
分 類 | LCC:QA8.9-10.3 DC23:511.3 |
書誌ID | 4001088594 |
ISBN | 9783540398615 |