Claude Kirchner, Hélène Kirchner
Proceedings of the 15th International Conference on Automated Deduction
CADE, 1998.

@proceedings{CADE-1998,
	address       = "Lindau, Germany",
	editor        = "Claude Kirchner and Hélène Kirchner",
	isbn          = "3-540-64675-2",
	publisher     = "{Springer-Verlag}",
	series        = "{Lecture Notes in Computer Science}",
	title         = "{Proceedings of the 15th International Conference on Automated Deduction}",
	volume        = 1421,
	year          = 1998,
}

Contents (37 items)

7 ×#proving
5 ×#theorem proving
4 ×#higher-order
3 ×#deduction
3 ×#logic
3 ×#verification
2 ×#algorithm
2 ×#analysis
2 ×#automation
2 ×#constraints

CADE-1998-Pfenning #deduction #linear #logic #reasoning

Reasoning About Deductions in Linear Logic (FP), pp. 1–2.

CADE-1998-FleuriotP #analysis #geometry #proving #standard #theorem proving

A Combination of Nonstandard Analysis and Geometry Theorem Proving, with Application to Newton’s Principia (JDF, LCP), pp. 3–16.

CADE-1998-FeveW #algebra #geometry #proving #theorem #using

Proving Geometric Theorems Using Clifford Algebra and Rewrite Rules (SF, DW), pp. 17–31.

CADE-1998-Fuchs #generative #similarity

System Description: Similarity-Based Lemma Generation for Model Elimination (MF), pp. 33–37.

CADE-1998-ArtsDFG #distributed #erlang #source code #verification

System Description: Verification of Distributed Erlang Programs (TA, MD, LÅF, DG), pp. 38–41.

CADE-1998-FuchsW

System Description: Cooperation in Model Elimination: CPTHEO (MF, AW), pp. 42–46.

CADE-1998-GorePSV #proving #smarttech #theorem proving

System Description: card TAP: The First Theorem Prover on a Smart Card (RG, JP, AS, HV), pp. 47–50.

CADE-1998-BeckertG

System Description: leanK 2.0 (BB, RG), pp. 51–55.

CADE-1998-BenzmullerK #higher-order

Extensional Higher-Order Resolution (CB, MK), pp. 56–71.

CADE-1998-Pagano #calculus #first-order #higher-order #reduction

X.R.S : Explicit Reduction Systems — A First-Order Calculus for Higher-Order Calculi (BP), pp. 72–87.

CADE-1998-BoudetC #confluence #equation #term rewriting

About the Confluence of Equational Pattern Rewrite Systems (AB, EC), pp. 88–102.

CADE-1998-Beeson #unification #λ-calculus

Unification in Lambda-Calculi with if-then-else (MB), pp. 103–118.

CADE-1998-Peltier #constraints #equation

System Description: An Equational Constraints Solver (NP), pp. 119–123.

CADE-1998-MazureSG #framework #platform #satisfiability

System Description: CRIL Platform for SAT (BM, LS, ÉG), pp. 124–128.

CADE-1998-RichardsonSG #higher-order #logic #proving #theorem proving

System Description: Proof Planning in Higher-Order Logic with Lambda-Clam (JR, AS, IG), pp. 129–133.

CADE-1998-SlindGBB #interface

System Description: An Interface Between CLAM and HOL (KS, MJCG, RJB, AB), pp. 134–138.

CADE-1998-BenzmullerK98a #higher-order #proving #theorem proving

System Description: LEO — A Higher-Order Theorem Prover (CB, MK), pp. 139–144.

CADE-1998-Waldmann

Superposition for Divisible Torsion-Free Abelian Groups (UW), pp. 144–159.

CADE-1998-BachmairG #strict

Strict Basic Superposition (LB, HG), pp. 160–174.

CADE-1998-BachmairGV #constraints #similarity

Elimination of Equality via Transformation with Ordering Constraints (LB, HG, AV), pp. 175–190.

CADE-1998-Nivelle

A Resolution Decision Procedure for the Guarded Fragment (HdN), pp. 191–204.

CADE-1998-Ohlbach #framework #reasoning #semantics

Combining Hilbert Style and Semantic Reasoning in a Resolution Framework (HJO), pp. 205–219.

CADE-1998-Kaufmann #verification

ACL2 Support for Verification Projects (MK), pp. 220–238.

CADE-1998-OliartS #algorithm #performance

A Fast Algorithm for Uniform Semi-Unification (AO, WS), pp. 239–253.

CADE-1998-BrauburgerG #analysis #evaluation #induction #termination

Termination Analysis by Inductive Evaluation (JB, JG), pp. 254–269.

CADE-1998-Crary #fixpoint #induction

Admissibility of Fixpoint Induction over Partial Types (KC), pp. 270–285.

CADE-1998-SchurmannP #automation #logic #proving #theorem proving

Automated Theorem Proving in a Simple Meta-Logic for LF (CS, FP), pp. 286–300.

CADE-1998-Pnueli #deduction #verification

Deductive vs. Model-Theoretic Approaches to Formal Verification (AP), p. 301.

CADE-1998-Malik #automation #deduction #finite #source code

Automated Deduction of Finite-State Control Programs for Reactive Systems (RM), pp. 302–316.

CADE-1998-KreitzHH #communication #development #proving

A Proof Environment for the Development of Group Communication Systems (CK, MH, JH), pp. 317–332.

CADE-1998-OhtaIH #on the #testing

On the Relationship Between Non-Horn Magic Sets and Relevancy Testing (YO, KI, RH), pp. 333–348.

CADE-1998-Thery #algorithm

A Certified Version of Buchberger’s Algorithm (LT), pp. 349–364.

CADE-1998-BishopA

Selectively Instantiating Definitions (MB, PBA), pp. 365–380.

CADE-1998-Letz #using

Using Matings for Pruning Connection Tableaux (RL), pp. 381–396.

CADE-1998-NonnengartRW #generative #normalisation #on the

On Generating Small Clause Normal Forms (AN, GR, CW), pp. 397–411.

CADE-1998-HortonS #canonical #named #process #rank

Rank/Activity: A Canonical Form for Binary Resolution (JDH, BS), pp. 412–426.

CADE-1998-Tammet #performance #towards

Towards Efficient Subsumption (TT), pp. 427–441.