15. CADE 1998: Lindau, Germany
Claude Kirchner, Hélène Kirchner (Eds.): Automated Deduction - CADE-15, 15th International Conference on Automated Deduction, Lindau, Germany, July 5-10, 1998, Proceedings. Springer 1998 Lecture Notes in Computer Science 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
- Rajeev Goré, Joachim Posegga, Andrew Slater, Harald Vogt: System Description: card TAP: The First Theorem Prover on a Smart Card. 47-50
Session 3:
- 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
- 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, 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
Session 8:
- Karl Crary: Admissibility of Fixpoint Induction over Partial Types. 270-285
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:
- 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
data released under the ODC-BY 1.0 license. See also our legal information page
last updated on 2013-06-18T211851 by the dblp team