Proceedings of the 20th International Conference on Automated Deduction
BibSLEIGH corpus
BibSLEIGH tags
BibSLEIGH bundles
BibSLEIGH people
EDIT!
CC-BY
Open Knowledge
XHTML 1.0 W3C Rec
CSS 2.1 W3C CanRec
email twitter

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

TEST
DBLP
Scholar
Full names Links ISxN
@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.

Bibliography of Software Language Engineering in Generated Hypertext (BibSLEIGH) is created and maintained by Dr. Vadim Zaytsev.
Hosted as a part of SLEBOK on GitHub.