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

• Συγγραφή απο Οργανισμό/Αρχή: SpringerLink (Online service)
• Άλλοι συγγραφείς: McCune, William (Επιμελητής έκδοσης, http://id.loc.gov/vocabulary/relators/edt)
• Μορφή: Ηλεκτρονική πηγή Ηλ. βιβλίο
• Γλώσσα: English
• Έκδοση: Berlin, Heidelberg : Springer Berlin Heidelberg : Imprint: Springer, 1997.
• Έκδοση: 1st ed. 1997.
• Σειρά: Lecture Notes in Artificial Intelligence ; 1249
• Θέματα: Artificial intelligence.; Architecture, Computer.; Mathematical logic.; Artificial Intelligence.; Computer System Implementation.; Mathematical Logic and Formal Languages.

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...

Πίνακας περιεχομένων:

• 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 logic theorem 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.