Automated Deduction - CADE-14

14th International Conference on Automated Deduction, Townsville, North Queensland, Australia, July 13 - 17, 1997, Proceedings

Häftad, Engelska, 1997

729 kr

Beställningsvara. Skickas inom 10-15 vardagar

Fri frakt för medlemmar vid köp för minst 249 kr.

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.

Produktinformation

Utgivningsdatum1997-06-18
Mått216 x 279 x 27 mm
Vikt727 g
FormatHäftad
SpråkEngelska
SerieLecture Notes in Computer Science
Antal sidor469
FörlagSpringer-Verlag Berlin and Heidelberg GmbH & Co. KG
ISBN9783540631040

Tillhör följande kategorier

Systemvetenskap och AI inom Data och it
Artificiell intelligens inom Data och it

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.