default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCID14th CADE 1997: Townsville, North Queensland, Australia
- William McCune:
Automated Deduction - CADE-14, 14th International Conference on Automated Deduction, Townsville, North Queensland, Australia, July 13-17, 1997, Proceedings. Lecture Notes in Computer Science 1249, Springer 1997, ISBN 3-540-63104-6
Session 1: Invited Lecture
- Wu Wen-Tsün:
The Char-Set Method and Its Applications to Automated Reasoning. 1-3
Session 2
- Irène Durand, Aart Middeldorp:
Decidable Call by Need Computations in term Rewriting (Extended Abstract). 4-18 - Franz Baader, Cesare Tinelli
:
A New Approach for Combining Decision Procedure for the Word Problem, and Its Connection to the Nelson-Oppen Combination Method. 19-33 - Joachim Niehren, Manfred Pinkal, Peter Ruhrberg:
On Equality Up-to Constraints over Finite Trees, Context Unification, and One-Step Rewriting. 34-48
Session 3: System Descriptions
- Robert Nieuwenhuis, José Miguel Rivero, Miguel Ángel Vallejo:
Dedan: A Kernel of Data Structures and Algorithms for Automated Deduction with Equality Clauses. 49-52 - Maria Paola Bonacina:
The Clause-Diffusion Theorem Prover Peers-mcd (System Description). 53-56 - Bernd I. Dahn, Jürgen Gehne, Th. Honigmann, Andreas Wolf:
Integration of Automated and Interactive Theorem Proving in ILP. 57-60 - Andreas Wolf, Johann Schumann:
ILF-SETHEO: Processing Model Elimination Proofs for Natural Language Output. 61-64 - Bernd Fischer, Johann Schumann:
SETHEO Goes Software Engineering: Application of ATP to Software Reuse. 65-68 - Wolfgang Reif, Gerhard Schellhorn, Kurt Stenzel:
Proving System Correctness with KIV 3.0. 69-72
Session 4
- Lu Yang, Hongguang Fu, Zhenbing Zeng:
A Practical Symbolic Algorithm for the Inverse Kinematics of 6R Manipulators with Simple Geometry. 73-86 - Johann Schumann:
Automatic Verification of Cryptographic Protocols with SETHEO. 87-100 - Nikolaj S. Bjørner, Mark E. Stickel, Tomás E. Uribe:
A Practical Integration of First-Order Reasoning and Decision Procedures. 101-115
Session 5
- Uwe Egly:
Some Pitfalls of LK-to-LJ Translations and How to Avoid Them. 116-130 - Daniel S. Korn, Christoph Kreitz:
Deciding Intuitionistic Propositional Logic via Translation into Classical Logic. 131-145
Session 6
- Koji Iwanuma:
Lemma Matching for a PTTP-based Top-down Theorem Prover. 146-160 - Olivier Roussel, Philippe Mathieu:
Exact Kanowledge Compilation in Predicate Calculus: The Partial Achievement Case. 161-175 - Ryuzo Hasegawa, Katsumi Inoue, Yoshihiko Ohta, Miyuki Koshimura:
Non-Horn Magic Sets to Incorporate Top-down Inference into Bottom-up Theorem Proving. 176-190
Session 7: Invited Lecture
- Moshe Y. Vardi:
Alternating Automata: Unifying Truth and Validity Checking for Temporal Logics. 191-206
Session 8
- Christoph Kreitz, Heiko Mantel, Jens Otten, Stephan Schmitt:
Connection-Based Proof Construction in Linear Logic. 207-221 - James Harland, David J. Pym:
Resource-Distribution via Boolean Constraint (Extended Abstract). 222-236 - Mary Cryan, Allan Ramsay:
Constructing a Normal Form for Property Theory. 237-251
Session 9: System Descriptions
- Christoph Benzmüller, Lassaad Cheikhrouhou, Detlef Fehrer, Armin Fiedler, Xiaorong Huang, Manfred Kerber, Michael Kohlhase, Karsten Konrad, Andreas Meier, Erica Melis, Wolf Schaarschmidt, Jörg H. Siekmann, Volker Sorge:
Omega: Towards a Mathematical Assistant. 252-255 - Thomas Kolbe, Jürgen Brauburger:
Plagiator - A Learning Prover. 256-259 - Dirk Fuchs, Matthias Fuchs:
CODE: A Powerful Prover for Problems of Condensed Detachment. 260-263 - Fausto Giunchiglia, Marco Roveri, Roberto Sebastiani:
A New Method for Testing Decision Procedures in Modal Logics. 264-267 - John K. Slaney:
Minlog: A Minimal Logic Theorem Prover. 268-271 - Hantao Zhang:
SATO: An Efficient Propositional Prover. 272-275
Session 10
- Louise A. Dennis, Alan Bundy, Ian Green:
Using A Generalisation Critic to Find Bisimulations for Coinductive Proofs. 276-290 - Dieter Hutter, Michael Kohlhase:
A Colored Version of the Lambda-Calculus. 291-305 - Seán Matthews:
A Practical Implementation of Simple Consequence Relations Using Inductive Definitions. 306-320
Session 11
- Harald Ganzinger, Christoph Meyer, Christoph Weidenbach:
Soft Typing for Ordered Resolution. 321-335 - Hans de Nivelle:
A Classification of Non-liftable Orders for Resolution. 336-350
Session 12
- Amy P. Felty, Douglas J. Howe:
Hybrid Interactive Theorem Proving Using Nuprl and HOL. 351-365 - Katherine A. Eastaughffe, Maris A. Ozols, Anthony Cant:
Proof Tactics for a Theory of State Machines in a Graphical Environment. 366-379 - David von Oheimb, Thomas F. Gritzner:
RALL: Machine-Supported Proofs for Relation Algebra. 380-394
Session 13: System Descriptions
- Jason J. Hickey:
Nuprl-Light: An Implementation Framework for Higher-Order Logics. 395-399 - Maris A. Ozols, Anthony Cant, Katherine A. Eastaughffe:
XIsabelle: A System Description. 400-403 - Helen Lowe, David Duncan:
XBarnacle: Making Theorem Provers More Accessible. 404-407 - Mathias Kettner, Norbert Eisinger:
The Tableau Browser SNARKS. 408-411 - Richard Bornat, Bernard Sufrin:
Jape: A Calculator for Animating Proof-on-Paper. 412-415
Session 14
- Matthias Fuchs:
Evolving Combinators. 416-430 - Gilles Défourneaux, Nicolas Peltier:
Partial Matching for Analogy Discovery in Proofs and Counter-Examples. 431-445 - Jürgen Ehrensberger, Claus Zinn:
DiaLog: A System for Dialogue Logic. 446-460
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
last updated on 2026-04-17 00:06 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
