Nothing Special   »   [go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

Automated Deduction - CADE-14

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

  • Conference proceedings
  • © 1997

Overview

Editors:
  1. William McCune
    View editor publications

    You can also search for this editor in PubMed   Google Scholar

Part of the book series: Lecture Notes in Computer Science (LNCS, volume 1249)

Part of the book sub series: Lecture Notes in Artificial Intelligence (LNAI)

Included in the following conference series:

Conference proceedings info: CADE 1997.

This is a preview of subscription content, log in via an institution to check access.

Access this book

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

eBook USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Other ways to access

Licence this eBook for your library

Institutional subscriptions

About this book

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.

Similar content being viewed by others

Keywords

Table of contents (45 papers)

  1. Front Matter

    Download chapter 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
Back to top

Other volumes

  1. Automated Deduction—CADE-14

Bibliographic Information

  • Book Title: Automated Deduction - CADE-14

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

  • Editors: William McCune

  • Series Title: Lecture Notes in Computer Science

  • DOI: https://doi.org/10.1007/3-540-63104-6

  • Publisher: Springer Berlin, Heidelberg

  • eBook Packages: Springer Book Archive

  • Copyright Information: Springer-Verlag Berlin Heidelberg 1997

  • Softcover ISBN: 978-3-540-63104-0Published: 18 June 1997

  • eBook ISBN: 978-3-540-69140-2Published: 06 July 2005

  • Series ISSN: 0302-9743

  • Series E-ISSN: 1611-3349

  • Edition Number: 1

  • Number of Pages: XV, 469

  • Topics: Artificial Intelligence, Computer System Implementation, Mathematical Logic and Formal Languages

Publish with us

Policies and ethics

Back to top

Search

Navigation