Robert Nieuwenhuis
Proceedings of the 20th International Conference on Automated Deduction
CADE, 2005.

@proceedings{CADE-2005,
	address       = "Tallinn, Estonia",
	editor        = "Robert Nieuwenhuis",
	isbn          = "3-540-28005-7",
	publisher     = "{Springer International Publishing}",
	series        = "{Lecture Notes in Computer Science}",
	title         = "{Proceedings of the 20th International Conference on Automated Deduction}",
	volume        = 3632,
	year          = 2005,
}

Contents (33 items)

5 ×#first-order
5 ×#logic
5 ×#proving
3 ×#similarity
3 ×#theorem proving
2 ×#calculus
2 ×#higher-order
2 ×#linear
2 ×#named
2 ×#reasoning

CADE-2005-Dowek #consistency #question #what

What Do We Know When We Know That a Theory Is Consistent? (GD), pp. 1–6.

CADE-2005-ContejeanC #first-order #logic #proving #similarity

Reflecting Proofs in First-Order Logic with Equality (EC, PC), pp. 7–22.

CADE-2005-Brown #reasoning #similarity #type system

Reasoning in Extensional Type Theory with Equality (CEB), pp. 23–37.

CADE-2005-UrbanT #higher-order

Nominal Techniques in Isabelle/HOL (CU, CT), pp. 38–53.

CADE-2005-Pientka #higher-order #logic programming

Tabling for Higher-Order Logic Programming (BP), pp. 54–68.

CADE-2005-ChaudhuriP #first-order #linear #logic #proving #theorem proving

A Focusing Inverse Method Theorem Prover for First-Order Linear Logic (KC, FP), pp. 69–83.

CADE-2005-Autexier #calculus

The CoRe Calculus (SA), pp. 84–98.

CADE-2005-Lev-AmiIRSSY #data type #first-order #linked data #logic #open data #reachability #simulation #using #verification

Simulating Reachability Using First-Order Logic with Applications to Verification of Linked Data Structures (TLA, NI, TWR, SS, SS, GY), pp. 99–115.

CADE-2005-DufayFM #data flow #information management #ml #privacy

Privacy-Sensitive Information Flow with JML (GD, APF, SM), pp. 116–130.

CADE-2005-ZhangSM #decidability #first-order

The Decidability of the First-Order Theory of Knuth-Bendix Order (TZ, HBS, ZM), pp. 131–148.

CADE-2005-LevyNV #unification

Well-Nested Context Unification (JL, JN, MV), pp. 149–163.

CADE-2005-GodoyT #linear #term rewriting #termination

Termination of Rewrite Systems with Shallow Right-Linear, Collapsing, and Right-Ground Rules (GG, AT), pp. 164–176.

CADE-2005-BechhoferHT #owl

The OWL Instance Store: System Description (SB, IH, DT), pp. 177–181.

CADE-2005-KonevWZ #logic #transitive

Temporal Logics over Transitive States (BK, FW, MZ), pp. 182–203.

CADE-2005-HustadtKS

Deciding Monodic Fragments by Temporal Resolution (UH, BK, RAS), pp. 204–218.

CADE-2005-Sofronie-Stokkermans #reasoning

Hierarchic Reasoning in Local Theory Extensions (VSS), pp. 219–234.

CADE-2005-CastelliniS #first-order #logic #proving #theorem proving

Proof Planning for First-Order Temporal Logic (CC, AS), pp. 235–249.

CADE-2005-MeierM #multi #proving #theorem proving

System Description: Multi A Multi-strategy Proof Planner (AM, EM), pp. 250–254.

CADE-2005-BryantS #verification

Decision Procedures Customized for Formal Verification (REB, SAS), pp. 255–259.

CADE-2005-KuncakNR #algebra #algorithm

An Algorithm for Deciding BAPA: Boolean Algebra with Presburger Arithmetic (VK, HHN, MCR), pp. 260–277.

CADE-2005-BaaderG

Connecting Many-Sorted Theories (FB, SG), pp. 278–294.

CADE-2005-McLaughlinH

A Proof-Producing Decision Procedure for Real Arithmetic (SM, JH), pp. 295–314.

CADE-2005-BozzanoBCJRSS

The MathSAT 3 System (MB, RB, AC, TAJ, PvR, SS, RS), pp. 315–321.

CADE-2005-Steel #api #constraints #deduction #modelling #security

Deduction with XOR Constraints in Security API Modelling (GS), pp. 322–336.

CADE-2005-VermaSS #complexity #equation #horn clause #on the

On the Complexity of Equational Horn Clauses (KNV, HS, TS), pp. 337–352.

CADE-2005-YorshM #generative

A Combination Method for Generating Interpolants (GY, MM), pp. 353–368.

CADE-2005-Benedetti #named

sKizzo: A Suite to Evaluate and Certify QBFs (MB), pp. 369–376.

CADE-2005-Truderung #protocol

Regular Protocols and Attacks with Regular Knowledge (TT), pp. 377–391.

CADE-2005-BaumgartnerT #calculus #evolution #similarity

The Model Evolution Calculus with Equality (PB, CT), pp. 392–408.

CADE-2005-FermullerP #representation

Model Representation via Contexts and Implicit Generalizations (CGF, RP), pp. 409–423.

CADE-2005-OgawaHO #incremental #proving

Proving Properties of Incremental Merkle Trees (MO, EH, SO), pp. 424–440.

CADE-2005-Zhang

Computer Search for Counterexamples to Wilkie’s Identity (JZ0), pp. 441–451.

CADE-2005-SinnerK #named

KRHyper — In Your Pocket (AS, TK), pp. 452–457.