8th International Conference on Automated Deduction: Oxford, England, July 27- August 1, 1986. Proceedings: Lecture Notes in Computer Science, cartea 230
Editat de Jörg H. Siekmannen Limba Engleză Paperback – iul 1986
Din seria Lecture Notes in Computer Science
- 20% Preț: 1040.03 lei
- 20% Preț: 333.46 lei
- 20% Preț: 335.08 lei
- 20% Preț: 444.17 lei
- 20% Preț: 238.01 lei
- 20% Preț: 333.46 lei
- 20% Preț: 438.69 lei
- Preț: 440.52 lei
- 20% Preț: 336.71 lei
- 20% Preț: 148.66 lei
- 20% Preț: 310.26 lei
- 20% Preț: 256.27 lei
- 20% Preț: 632.22 lei
- 17% Preț: 427.22 lei
- 20% Preț: 641.78 lei
- 20% Preț: 307.71 lei
- 20% Preț: 1053.45 lei
- 20% Preț: 579.56 lei
- Preț: 373.56 lei
- 20% Preț: 330.23 lei
- 15% Preț: 429.74 lei
- 20% Preț: 607.39 lei
- 20% Preț: 538.29 lei
- Preț: 389.48 lei
- 20% Preț: 326.98 lei
- 20% Preț: 1386.07 lei
- 20% Preț: 1003.66 lei
- 20% Preț: 567.60 lei
- 20% Preț: 575.48 lei
- 20% Preț: 571.63 lei
- 20% Preț: 747.79 lei
- 15% Preț: 568.74 lei
- 17% Preț: 360.19 lei
- 20% Preț: 504.57 lei
- 20% Preț: 172.69 lei
- 20% Preț: 369.12 lei
- 20% Preț: 346.40 lei
- 20% Preț: 574.05 lei
- Preț: 402.62 lei
- 20% Preț: 584.40 lei
- 20% Preț: 747.79 lei
- 20% Preț: 809.19 lei
- 20% Preț: 649.49 lei
- 20% Preț: 343.16 lei
- 20% Preț: 309.90 lei
- 20% Preț: 122.89 lei
Preț: 404.48 lei
Nou
Puncte Express: 607
Preț estimativ în valută:
77.41€ • 80.41$ • 64.30£
77.41€ • 80.41$ • 64.30£
Carte tipărită la comandă
Livrare economică 03-17 februarie 25
Preluare comenzi: 021 569.72.76
Specificații
ISBN-13: 9783540167808
ISBN-10: 3540167803
Pagini: 724
Ilustrații: XII, 716 p.
Dimensiuni: 155 x 235 x 38 mm
Greutate: 1 kg
Ediția:1986
Editura: Springer Berlin, Heidelberg
Colecția Springer
Seria Lecture Notes in Computer Science
Locul publicării:Berlin, Heidelberg, Germany
ISBN-10: 3540167803
Pagini: 724
Ilustrații: XII, 716 p.
Dimensiuni: 155 x 235 x 38 mm
Greutate: 1 kg
Ediția:1986
Editura: Springer Berlin, Heidelberg
Colecția Springer
Seria Lecture Notes in Computer Science
Locul publicării:Berlin, Heidelberg, Germany
Public țintă
ResearchCuprins
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 usinggeneralization 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 resolutiontheorem 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.