Andrei Voronkov
Proceedings of the 18th International Conference on Automated Deduction
CADE, 2002.

@proceedings{CADE-2002,
	address       = "Copenhagen, Denmark",
	editor        = "Andrei Voronkov",
	isbn          = "3-540-43931-5",
	publisher     = "{Springer International Publishing}",
	series        = "{Lecture Notes in Computer Science}",
	title         = "{Proceedings of the 18th International Conference on Automated Deduction}",
	volume        = 2392,
	year          = 2002,
}

Contents (40 items)

8 ×#logic
6 ×#proving
4 ×#reasoning
3 ×#generative
3 ×#satisfiability
2 ×#approach
2 ×#named
2 ×#order
2 ×#performance
2 ×#symmetry

CADE-2002-Horrocks #logic #reasoning #theory and practice

Reasoning with Expressive Description Logics: Theory and Practice (IH), pp. 1–15.

CADE-2002-PanSV

BDD-Based Decision Procedures for K (GP, US, MYV), pp. 16–30.

CADE-2002-BernardL #logic

Temporal Logic for Proof-Carrying Code (AB, PL), pp. 31–46.

CADE-2002-SchneckN #approach #scalability

A Gradual Approach to a More Trustworthy, Yet Scalable, Proof-Carrying Code (RRS, GCN), pp. 47–62.

CADE-2002-Strecker #compilation #java #verification

Formal Verification of a Java Compiler in Isabelle (MS), pp. 63–77.

CADE-2002-Egly #logic

Embedding Lax Logic into Intuitionistic Logic (UE), pp. 78–93.

CADE-2002-Larchey-Wendling #logic

Combining Proof-Search and Counter-Model Construction for Deciding Gödel-Dummett Logic (DLW), pp. 94–110.

CADE-2002-GalmicheM #logic #proving

Connection-Based Proof Search in Propositional BI Logic (DG, DM), pp. 111–128.

CADE-2002-Moller #difference #library #named #quantifier

DDDLIB: A Library for Solving Quantified Difference Inequalities (JBM), pp. 129–133.

CADE-2002-Hurd #first-order #interface #logic

An LCF-Style Interface between HOL and First-Order Logic (JH), pp. 134–138.

CADE-2002-ZimmerK #distributed #reasoning

System Description: The MathWeb Software Bus for Distributed Mathematical Reasoning (JZ, MK), pp. 139–143.

CADE-2002-SiekmannBBCFFHKMMMNPSUWZ #development #proving

Proof Development with OMEGA (JHS, CB, VB, LC, AF, AF, HH, MK, AM, EM, MM, IN, MP, VS, CU, CPW, JZ), pp. 144–149.

CADE-2002-JamnikKP

Learn Omega-matic: System Description (MJ, MK, MP), pp. 150–155.

CADE-2002-ArecesH #hybrid #logic

HyLoRes 1.0: Direct Resolution for Hybrid Logics (CA, JH), pp. 156–160.

CADE-2002-Goldberg #satisfiability #testing

Testing Satisfiability of CNF Formulas by Computing a Stable Set of Points (EG), pp. 161–180.

CADE-2002-Tour #heuristic #symmetry

A Note on Symmetry Heuristics in SEM (TBdlT), pp. 181–194.

CADE-2002-AudemardBCKS #approach #linear #satisfiability

A SAT Based Approach for Solving Formulas over Boolean and Linear Mathematical Propositions (GA, PB, AC, AK, RS), pp. 195–210.

CADE-2002-Ahrendt #data type #deduction #fault #generative #specification #using

Deductive Search for Errors in Free Data Type Specifications Using Model Generation (WA), pp. 211–225.

CADE-2002-AudemardB #finite #generative #reasoning #symmetry

Reasoning by Symmetry and Function Ordering in Finite Model Generation (GA, BB), pp. 226–240.

CADE-2002-GramlichP #algorithm #aspect-oriented #equation #modelling

Algorithmic Aspects of Herbrand Models Represented by Ground Atoms with Ground Equations (BG, RP), pp. 241–259.

CADE-2002-GeorgievaHS #decidability

A New Clausal Class Decidable by Hyperresolution (LG, UH, RAS), pp. 260–274.

CADE-2002-WeidenbachBHKTT

S PASS Version 2.0 (CW, UB, TH, EK, CT, DT), pp. 275–279.

CADE-2002-SchulzS

System Description: GrAnDe 1.0 (SS, GS), pp. 280–284.

CADE-2002-Colton #generative #theorem

The HR Program for Theorem Generation (SC), pp. 285–289.

CADE-2002-WhalenSF #automation #certification #named #synthesis

AutoBayes/CC — Combining Program Synthesis with Automatic Code Certification — System Description (MWW, JS, BF), pp. 290–294.

CADE-2002-ZhangM #performance #satisfiability

The Quest for Efficient Boolean Satisfiability Solvers (LZ, SM), pp. 295–313.

CADE-2002-BorrallerasLR #order #recursion

Recursive Path Orderings Can Be Context-Sensitive (CB, SL, AR), pp. 314–331.

CADE-2002-Ganzinger

Shostak Light (HG), pp. 332–346.

CADE-2002-FordS #verification

Formal Verification of a Combination Decision Procedure (JF, NS), pp. 347–362.

CADE-2002-Zarba #integer #multi

Combining Multisets with Integers (CGZ), pp. 363–376.

CADE-2002-Paulson #case study #reasoning #theorem

The Reflection Theorem: A Study in Meta-theoretic Reasoning (LCP), pp. 377–391.

CADE-2002-StumpD #framework #logic #performance #proving

Faster Proof Checking in the Edinburgh Logical Framework (AS, DLD), pp. 392–407.

CADE-2002-Brown #higher-order #proving #set #theorem proving

Solving for Set Variables in Higher-Order Theorem Proving (CEB), pp. 408–422.

CADE-2002-KupfermanSV #calculus #complexity

The Complexity of the Graded µ-Calculus (OK, US, MYV), pp. 423–437.

CADE-2002-MouraRS #bound #infinity #lazy evaluation #model checking #proving #theorem proving

Lazy Theorem Proving for Bounded Model Checking over Infinite Domains (LMdM, HR, MS), pp. 438–455.

CADE-2002-BofillR #order

Well-Foundedness Is Sufficient for Completeness of Ordered Paramodulation (MB, AR), pp. 456–470.

CADE-2002-LynchM

Basic Syntactic Mutation (CL, BM), pp. 471–485.

CADE-2002-HillenbrandL

The Next W ALDMEISTER Loop (TH, BL), pp. 486–500.

CADE-2002-Andreoli #middleware #paradigm

Focussing Proof-Net Construction as a Middleware Paradigm (JMA), pp. 501–516.

CADE-2002-Baaz #analysis #proving

Proof Analysis by Resolution (MB), pp. 517–532.