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

The char-set method and its applications to automated reasoning....Pages 1-3
Decidable call by need computations in term rewriting (extended abstract)....Pages 4-18
A New approach for combining decision procedures for the word problem, and its connection to the Nelson-Oppen combination method....Pages 19-33
On equality up-to constraints over finite trees, context unification, and one-step rewriting....Pages 34-48
Dedam: A kernel of data structures and algorithms for automated deduction with equality clauses....Pages 49-52
The Clause-Diffusion theorem prover Peers-mcd (system description)....Pages 53-56
Integration of automated and interactive theorem proving in ILF....Pages 57-60
ILF-SETHEO....Pages 61-64
SETHEO goes software engineering: Application of ATP to software reuse....Pages 65-68
Proving System Correctness with KIV 3.0....Pages 69-72
A practical symbolic algorithm for the inverse kinematics of 6R manipulators with simple geometry....Pages 73-86
Automatic verification of cryptographic protocols with SETHEO....Pages 87-100
A practical integration of first-order reasoning and decision procedures....Pages 101-115
Some pitfalls of LK-to-LJ translations and how to avoid them....Pages 116-130
Deciding intuitionistic propositional logic via translation into classical logic....Pages 131-145
Lemma matching for a PTTP-based top-down theorem prover....Pages 146-160
Exact knowledge compilation in predicate calculus: The partial achievement case....Pages 161-175
Non-horn magic sets to incorporate top-down inference into bottom-up theorem proving....Pages 176-190
Alternating automata: Unifying truth and validity checking for temporal logics....Pages 191-206
Connection-based proof construction in linear logic....Pages 207-221
Resource-distribution via Boolean constraints....Pages 222-236
Constructing a normal form for Property Theory....Pages 237-251
Ωmega: Towards a mathematical assistant....Pages 252-255
Plagiator — A learning prover....Pages 256-259
CODE: A powerful prover for problems of condensed detachment....Pages 260-263
A new method for testing decision procedures in modal logics....Pages 264-267
Minlog: A minimal logic theorem prover....Pages 268-271
SATO: An efficient prepositional prover....Pages 272-275
Using a generalisation critic to find bisimulations for coinductive proofs....Pages 276-290
A colored version of the λ-calculus....Pages 291-305
A practical implementation of simple consequence relations using inductive definitions....Pages 306-320
Soft typing for ordered resolution....Pages 321-335
A classification of non-liftable orders for resolution....Pages 336-350
Hybrid interactive theorem proving using nuprl and HOL....Pages 351-365
Proof tactics for a theory of state machines in a graphical environment....Pages 366-379
RALL: Machine-supported proofs for relation algebra....Pages 380-394
Nuprl-Light: An implementation framework for higher-order logics....Pages 395-399
XIsabelle: A system description....Pages 400-403
XBarnacle: Making theorem provers more accessible....Pages 404-407
The tableau browser SNARKS....Pages 408-411
Jape: A calculator for animating proof-on-paper....Pages 412-415
Evolving combinators....Pages 416-430
Partial matching for analogy discovery in proofs and counter-examples....Pages 431-445
Dialog....Pages 446-460