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