## 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)

- 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.

5 ×#first-order

5 ×#logic

5 ×#proving

3 ×#similarity

3 ×#theorem proving

2 ×#calculus

2 ×#higher-order

2 ×#linear

2 ×#named

2 ×#reasoning

5 ×#logic

5 ×#proving

3 ×#similarity

3 ×#theorem proving

2 ×#calculus

2 ×#higher-order

2 ×#linear

2 ×#named

2 ×#reasoning