Automated Deduction - CADE-14

1. Front Matter

   PDF

2. The char-set method and its applications to automated reasoning

   • Wu Wen-Tsün

   Pages 1-3

3. Decidable call by need computations in term rewriting (extended abstract)

   • Irène Durand, Aart Middeldorp

   Pages 4-18

4. A New approach for combining decision procedures for the word problem, and its connection to the Nelson-Oppen combination method

   • Franz Baader, Cesare Tinelli

   Pages 19-33

5. On equality up-to constraints over finite trees, context unification, and one-step rewriting

   • Joachim Niehren, Manfred Pinkal, Peter Ruhrberg

   Pages 34-48

6. Dedam: A kernel of data structures and algorithms for automated deduction with equality clauses

   • Robert Nieuwenhuis, José Miguel Rivero, Miguel Angel Vallejo

   Pages 49-52

7. The Clause-Diffusion theorem prover Peers-mcd (system description)

   • Maria Paola Bonacina

   Pages 53-56

8. Integration of automated and interactive theorem proving in ILF

   • B. I. Dahn, J. Gehne, Th. Honigmann, A. Wolf

   Pages 57-60

9. ILF-SETHEO

   • Andreas Wolf, Johann Schumann

   Pages 61-64

10. SETHEO goes software engineering: Application of ATP to software reuse

    • Bernd Fischer, Johann M. Ph. Schumann

    Pages 65-68

11. Proving System Correctness with KIV 3.0

    • Wolfgang Reif, Gerhard Schellhorn, Kurt Stenzel

    Pages 69-72

12. A practical symbolic algorithm for the inverse kinematics of 6R manipulators with simple geometry

    • Lu Yang, Hongguang Fu, Zhenbing Zeng

    Pages 73-86

13. Automatic verification of cryptographic protocols with SETHEO

    • Johann Schumann

    Pages 87-100

14. A practical integration of first-order reasoning and decision procedures

    • Nikolaj S. Bjørner, Mark E. Stickel, Tomás E. Uribe

    Pages 101-115

15. Some pitfalls of LK-to-LJ translations and how to avoid them

    • Uwe Egly

    Pages 116-130

16. Deciding intuitionistic propositional logic via translation into classical logic

    • Daniel S. Korn, Christoph Kreitz

    Pages 131-145

17. Lemma matching for a PTTP-based top-down theorem prover

    • Koji Iwanuma

    Pages 146-160

18. Exact knowledge compilation in predicate calculus: The partial achievement case

    • Olivier Roussel, Philippe Mathieu

    Pages 161-175

19. Non-horn magic sets to incorporate top-down inference into bottom-up theorem proving

    • Ryuzo Hasegawa, Katsumi Inoue, Yoshihiko Ohta, Miyuki Koshimura

    Pages 176-190

20. Alternating automata: Unifying truth and validity checking for temporal logics

    • Moshe Y. Vardi

    Pages 191-206

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.

• AI logics
• Automatische Deduktion
• Automatisches Schließen
• KI-Logiken
• Theorem-Beweise
• artificial intelligence
• automated deduction
• automated reasoning
• automatic verification
• theorem proving
• verification

Policies and ethics