Automated Deduction - CADE-14 de William McCune

Automated Deduction - CADE-14: 14th International Conference on Automated Deduction, Townsville, North Queensland, Australia, July 13 - 17, 1997, Proceedings: Lecture Notes in Computer Science, cartea 1249

William McCune

en Limba Engleză Paperback – 18 iun 1997

This book constitutes the strictly refereed proceedings of the 14th International Conference on Automated Deduction, CADE-14, held in Townsville, North Queensland, Australia, in July 1997.
The volume presents 25 revised full papers selected from a total of 87 submissions; also included are 17 system descriptions and two invited contributions. The papers cover a wide range of current issues in the area including resolution, term rewriting, unification theory, induction, high-order logics, nonstandard logics, AI methods, and applications to software verification, geometry, and social science.

Citește tot Restrânge

Din seria Lecture Notes in Computer Science

20%

Preț: 1061^.55 lei
20%

Preț: 307^.71 lei
20%

Preț: 438^.69 lei
20%

Preț: 645^.28 lei
Preț: 410^.88 lei
15%

Preț: 580^.46 lei
17%

Preț: 427^.22 lei
20%

Preț: 596^.46 lei
Preț: 381^.21 lei
20%

Preț: 353^.50 lei
20%

Preț: 1414^.79 lei
20%

Preț: 309^.90 lei
20%

Preț: 583^.40 lei
20%

Preț: 1075^.26 lei
20%

Preț: 310^.26 lei
20%

Preț: 655^.02 lei
20%

Preț: 580^.93 lei
20%

Preț: 340^.32 lei
15%

Preț: 438^.59 lei
20%

Preț: 591^.51 lei
20%

Preț: 649^.49 lei
20%

Preț: 337^.00 lei
Preț: 449^.57 lei
20%

Preț: 607^.39 lei
20%

Preț: 1024^.44 lei
20%

Preț: 579^.30 lei
20%

Preț: 763^.23 lei
20%

Preț: 453^.32 lei
20%

Preț: 575^.48 lei
20%

Preț: 585^.88 lei
20%

Preț: 825^.93 lei
20%

Preț: 763^.23 lei
17%

Preț: 360^.19 lei
20%

Preț: 1183^.14 lei
20%

Preț: 340^.32 lei
20%

Preț: 504^.57 lei
20%

Preț: 369^.12 lei
20%

Preț: 583^.40 lei
20%

Preț: 343^.62 lei
20%

Preț: 350^.21 lei
20%

Preț: 764^.89 lei
20%

Preț: 583^.40 lei
Preț: 389^.48 lei
20%

Preț: 341^.95 lei
20%

Preț: 238^.01 lei
20%

Preț: 538^.29 lei

Specificații

ISBN-13: 9783540631040
ISBN-10: 3540631046
Pagini: 484
Ilustrații: XIV, 462 p.
Dimensiuni: 216 x 279 x 25 mm
Greutate: 0.67 kg
Ediția:1997
Editura: Springer Berlin, Heidelberg
Colecția Springer
Seriile Lecture Notes in Computer Science, Lecture Notes in Artificial Intelligence

Locul publicării:Berlin, Heidelberg, Germany

Cuprins

The char-set method and its applications to automated reasoning.- Decidable call by need computations in term rewriting (extended abstract).- A New approach for combining decision procedures for the word problem, and its connection to the Nelson-Oppen combination method.- On equality up-to constraints over finite trees, context unification, and one-step rewriting.- Dedam: A kernel of data structures and algorithms for automated deduction with equality clauses.- The Clause-Diffusion theorem prover Peers-mcd (system description).- Integration of automated and interactive theorem proving in ILF.- ILF-SETHEO.- SETHEO goes software engineering: Application of ATP to software reuse.- Proving System Correctness with KIV 3.0.- A practical symbolic algorithm for the inverse kinematics of 6R manipulators with simple geometry.- Automatic verification of cryptographic protocols with SETHEO.- A practical integration of first-order reasoning and decision procedures.- Some pitfalls of LK-to-LJ translations and how to avoid them.- Deciding intuitionistic propositional logic via translation into classical logic.- Lemma matching for a PTTP-based top-down theorem prover.- Exact knowledge compilation in predicate calculus: The partial achievement case.- Non-horn magic sets to incorporate top-down inference into bottom-up theorem proving.- Alternating automata: Unifying truth and validity checking for temporal logics.- Connection-based proof construction in linear logic.- Resource-distribution via Boolean constraints.- Constructing a normal form for Property Theory.- ?mega: Towards a mathematical assistant.- Plagiator — A learning prover.- CODE: A powerful prover for problems of condensed detachment.- A new method for testing decision procedures in modal logics.- Minlog: A minimal logictheorem prover.- SATO: An efficient prepositional prover.- Using a generalisation critic to find bisimulations for coinductive proofs.- A colored version of the ?-calculus.- A practical implementation of simple consequence relations using inductive definitions.- Soft typing for ordered resolution.- A classification of non-liftable orders for resolution.- Hybrid interactive theorem proving using nuprl and HOL.- Proof tactics for a theory of state machines in a graphical environment.- RALL: Machine-supported proofs for relation algebra.- Nuprl-Light: An implementation framework for higher-order logics.- XIsabelle: A system description.- XBarnacle: Making theorem provers more accessible.- The tableau browser SNARKS.- Jape: A calculator for animating proof-on-paper.- Evolving combinators.- Partial matching for analogy discovery in proofs and counter-examples.- Dialog.