+612 9045 4394
Automated Deduction - Cade-14 : 14th International Conference on Automated Deduction, Townsville, North Queensland, Australia, July 13 - 17, 1997, Proceedings - William McCune

Automated Deduction - Cade-14

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

By: William McCune (Editor)


Published: 18th June 1997
Ships: 5 to 9 business days
5 to 9 business days
or 4 easy payments of $36.76 with Learn more

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.

The Char-Set Method and Its Applications to Automated Reasoningp. 1
Decidable Call by Need Computations in Term Rewritingp. 4
A New Approach for Combining Decision Procedures for the Word Problem, and Its Connection to the Nelson-Oppen Combination Methodp. 19
On Equality Up-to Constraints over Finite Trees, Context Unification, and One-Step Rewritingp. 34
Dedam: A Kernel of Data Structures and Algorithms for Automated Deduction with Equality Clausesp. 49
The Clause-Diffusion Theorem Prover Peers-mcdp. 53
Integration of Automated and Interactive Theorem Proving in ILFp. 57
ILF-SETHEO: Processing Model Elimination Proofs for Natural Language Outputp. 61
SETHEO Goes Software Engineering: Application of ATP to Software Reusep. 65
Proving System Correctness with KIV 3.0p. 69
A Practical Symbolic Algorithm for the Inverse Kinematics of 6R Manipulators with Simple Geometryp. 73
Automatic Verification of Cryptographic Protocols with SETHEOp. 87
A Practical Integration of First-Order Reasoning and Decision Proceduresp. 101
Some Pitfalls of LK-to-LJ Translations and How to Avoid Themp. 116
Deciding Intuitionistic Propositional Logic via Translation into Classical Logicp. 131
Lemma Matching for a PTTP-based Top-down Theorem Proverp. 146
Exact Knowledge Compilation in Predicate Calculus: The Partial Achievement Casep. 161
Non-Horn Magic Sets to Incorporate Top-down Inference into Bottom-up Theorem Provingp. 176
Alternating Automata: Unifying Truth and Validity Checking for Temporal Logicsp. 191
Connection-Based Proof Construction in Linear Logicp. 207
Resource-Distribution via Boolean Constraintsp. 222
Constructing a Normal Form for Property Theoryp. 237
[Omega]MEGA: Towards a Mathematical Assistantp. 252
PLAGIATOR: A Learning Proverp. 256
CODE: A Powerful Prover for Problems of Condensed Detachmentp. 260
A New Method for Testing Decision Procedures in Modal Logicsp. 264
MINLOG: A Minimal Logic Theorem Proverp. 268
SATO: An Efficient Propositional Proverp. 272
Using a Generalisation Critic to Find Bisimulations for Coinductive Proofsp. 276
A Colored Version of the [lambda]-Calculusp. 291
A Practical Implementation of Simple Consequence Relations Using Inductive Definitionsp. 306
Soft Typing for Ordered Resolutionp. 321
A Classification of Non-Liftable Orders for Resolutionp. 336
Hybrid Interactive Theorem Proving Using Nuprl and HOLp. 351
Proof Tactics for a Theory of State Machines in a Graphical Environmentp. 366
RALL: Machine-Supported Proofs for Relation Algebrap. 380
Nuprl-Light: An Implementation Framework for Higher-Order Logicsp. 395
XIsabelle: A System Descriptionp. 400
XBarnacle: Making Theorem Provers More Accessiblep. 404
The Tableau Browser SNARKSp. 408
Jape: A Calculator for Animating Proof-on-Paperp. 412
Evolving Combinatorsp. 416
Partial Matching for Analogy Discovery in Proofs and Counter-examplesp. 431
DIALOG: A System for Dialogue Logicp. 446
Author Indexp. 461
Table of Contents provided by Blackwell. All Rights Reserved.

ISBN: 9783540631040
ISBN-10: 3540631046
Series: Lecture Notes in Computer Science
Audience: General
Format: Paperback
Language: English
Number Of Pages: 469
Published: 18th June 1997
Publisher: Springer-Verlag Berlin and Heidelberg Gmbh & Co. Kg
Country of Publication: DE
Dimensions (cm): 23.39 x 15.6  x 2.46
Weight (kg): 0.67