default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCID15th CADE 1998: Lindau, Germany
- Claude Kirchner, Hélène Kirchner:
Automated Deduction - CADE-15, 15th International Conference on Automated Deduction, Lindau, Germany, July 5-10, 1998, Proceedings. Lecture Notes in Computer Science 1421, Springer 1998, ISBN 3-540-64675-2
Session 1:
- Frank Pfenning:
Reasoning About Deductions in Linear Logic (Abstract of Invited Talk). 1-2 - Jacques D. Fleuriot
, Lawrence C. Paulson:
A Combination of Nonstandard Analysis and Geometry Theorem Proving, with Application to Newton's Principia. 3-16 - Stéphane Fèvre, Dongming Wang:
Proving Geometric Theorems Using Clifford Algebra and Rewrite Rules. 17-31
Session 2: System Descriptions
- Marc Fuchs:
System Description: Similarity-Based Lemma Generation for Model Elimination. 33-37 - Thomas Arts, Mads Dam, Lars-Åke Fredlund, Dilian Gurov:
System Description: Verification of Distributed Erlang Programs. 38-41 - Marc Fuchs, Andreas Wolf:
System Description: Cooperation in Model Elimination: CPTHEO. 42-46 - Rajeev Goré, Joachim Posegga, Andrew Slater, Harald Vogt:
System Description: card TAP: The First Theorem Prover on a Smart Card. 47-50 - Bernhard Beckert, Rajeev Goré:
System Description: leanK 2.0. 51-55
Session 3:
- Christoph Benzmüller, Michael Kohlhase:
Extensional Higher-Order Resolution. 56-71 - Bruno Pagano:
X.R.S : Explicit Reduction Systems - A First-Order Calculus for Higher-Order Calculi. 72-87 - Alexandre Boudet, Evelyne Contejean:
About the Confluence of Equational Pattern Rewrite Systems. 88-102
Session 4:
- Michael Beeson:
Unification in Lambda-Calculi with if-then-else. 103-118
System Descriptions
- Nicolas Peltier:
System Description: An Equational Constraints Solver. 119-123 - Bertrand Mazure, Lakhdar Sais, Éric Grégoire:
System Description: CRIL Platform for SAT. 124-128 - Julian Richardson, Alan Smaill, Ian Green:
System Description: Proof Planning in Higher-Order Logic with Lambda-Clam. 129-133 - Konrad Slind, Michael J. C. Gordon, Richard J. Boulton, Alan Bundy:
System Description: An Interface Between CLAM and HOL. 134-138 - Christoph Benzmüller, Michael Kohlhase:
System Description: LEO - A Higher-Order Theorem Prover. 139-144
Session 5:
- Uwe Waldmann:
Superposition for Divisible Torsion-Free Abelian Groups. 144-159 - Leo Bachmair, Harald Ganzinger:
Strict Basic Superposition. 160-174 - Leo Bachmair, Harald Ganzinger, Andrei Voronkov:
Elimination of Equality via Transformation with Ordering Constraints. 175-190
Session 6:
- Hans de Nivelle:
A Resolution Decision Procedure for the Guarded Fragment. 191-204 - Hans Jürgen Ohlbach:
Combining Hilbert Style and Semantic Reasoning in a Resolution Framework. 205-219
Session 7:
- Matt Kaufmann:
ACL2 Support for Verification Projects (Invited Talk). 220-238 - Alberto Oliart, Wayne Snyder:
A Fast Algorithm for Uniform Semi-Unification. 239-253
Session 8:
- Jürgen Brauburger, Jürgen Giesl:
Termination Analysis by Inductive Evaluation. 254-269 - Karl Crary:
Admissibility of Fixpoint Induction over Partial Types. 270-285 - Carsten Schürmann, Frank Pfenning:
Automated Theorem Proving in a Simple Meta-Logic for LF. 286-300
Session 9:
- Amir Pnueli:
Deductive vs. Model-Theoretic Approaches to Formal Verification (Abstract of Invited Talk). 301 - Robi Malik:
Automated Deduction of Finite-State Control Programs for Reactive Systems. 302-316
Session 10:
- Christoph Kreitz, Mark Hayden, Jason Hickey:
A Proof Environment for the Development of Group Communication Systems. 317-332 - Yoshihiko Ohta, Katsumi Inoue, Ryuzo Hasegawa:
On the Relationship Between Non-Horn Magic Sets and Relevancy Testing. 333-348 - Laurent Théry:
A Certified Version of Buchberger's Algorithm. 349-364
Session 11:
- Matthew Bishop, Peter B. Andrews:
Selectively Instantiating Definitions. 365-380 - Reinhold Letz:
Using Matings for Pruning Connection Tableaux. 381-396
Session 12:
- Andreas Nonnengart, Georg Rock, Christoph Weidenbach:
On Generating Small Clause Normal Forms. 397-411 - Joseph Douglas Horton, Bruce Spencer:
Rank/Activity: A Canonical Form for Binary Resolution. 412-426 - Tanel Tammet:
Towards Efficient Subsumption. 427-441
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-29 00:09 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:
