BibSLEIGH — Proceedings of the 22nd International Conference on Automated Deduction

Renate A. Schmidt
Proceedings of the 22nd International Conference on Automated Deduction
CADE, 2009.

TEST

@proceedings{CADE-2009,
	address       = "Montreal, Canada",
	doi           = "10.1007/978-3-642-02959-2",
	editor        = "Renate A. Schmidt",
	isbn          = "978-3-642-02958-5",
	publisher     = "{Springer International Publishing}",
	series        = "{Lecture Notes in Computer Science}",
	title         = "{Proceedings of the 22nd International Conference on Automated Deduction}",
	volume        = 5663,
	year          = 2009,
}

Contents (35 items)

CADE-2009-Rinard #proving #reasoning: Integrated Reasoning and Proof Choice Point Selection in the Jahob System — Mechanisms for Program Survival (MCR), pp. 1–16.
CADE-2009-BaumgartnerW #evolution: Superposition and Model Evolution Combined (PB, UW), pp. 17–34.
CADE-2009-BonacinaLM #on the #proving #satisfiability #theorem proving: On Deciding Satisfiability by DPLL(G+T) and Unsound Theorem Proving (MPB, CL, LMdM), pp. 35–50.
CADE-2009-NicoliniRR: Combinable Extensions of Abelian Groups (EN, CR, MR), pp. 51–66.
CADE-2009-Sofronie-Stokkermans #locality: Locality Results for Certain Extensions of Theories with Bridging Functions (VSS), pp. 67–83.
CADE-2009-SebastianiV #analysis #axiom #encoding #lightweight #logic: Axiom Pinpointing in Lightweight Description Logics via Horn-SAT Encoding and Conflict Analysis (RS, MV), pp. 84–99.
CADE-2009-GregoireMP #question #set: Does This Set of Clauses Overlap with at Least One MUS? (ÉG, BM, CP), pp. 100–115.
CADE-2009-SutcliffeBBT #automation #development #higher-order #logic #proving #theorem proving: Progress in the Development of Automated Theorem Proving for Higher-Order Logic (GS, CB, CEB, FT), pp. 116–130.
CADE-2009-IhlemannS: System Description: H-PILoT (CI, VSS), pp. 131–139.
CADE-2009-WeidenbachDFKSW: SPASS Version 3.5 (CW, DD, AF, RK, MS, PW), pp. 140–145.
CADE-2009-BensaidCP #integer #named #proving #theorem proving: Dei: A Theorem Prover for Terms with Integer Exponents (HB, RC, NP), pp. 146–150.
CADE-2009-BoutonODF #named #performance: veriT: An Open, Trustable and Efficient SMT-Solver (TB, DCBdO, DD, PF), pp. 151–156.
CADE-2009-RoedererPS #axiom #named: Divvy: An ATP Meta-system Based on Axiom Relevance Ordering (AR, YP, GS), pp. 157–162.
CADE-2009-Korovin #automation #reasoning #theory and practice: Instantiation-Based Automated Reasoning: From Theory to Practice (KK), pp. 163–166.
CADE-2009-CimattiGS #generative: Interpolant Generation for UTVPI (AC, AG, RS), pp. 167–182.
CADE-2009-GoelKT: Ground Interpolation for Combined Theories (AG, SK, CT), pp. 183–198.
CADE-2009-KovacsV: Interpolation and Symbol Elimination (LK, AV), pp. 199–213.
CADE-2009-LahiriQ #abstraction #algorithm #complexity: Complexity and Algorithms for Monomial and Clausal Predicate Abstraction (SKL, SQ), pp. 214–229.
CADE-2009-McLaughlinP #performance #proving #theorem proving: Efficient Intuitionistic Theorem Proving with the Polarized Inverse Method (SM, FP), pp. 230–244.
CADE-2009-ZhangHD #calculus: A Refined Resolution Calculus for CTL (LZ, UH, CD), pp. 245–260.
CADE-2009-LudwigH #reasoning: Fair Derivations in Monodic Temporal Reasoning (ML, UH), pp. 261–276.
CADE-2009-FalkeK #analysis #approach #automation #imperative #source code #term rewriting #termination: A Term Rewriting Approach to the Automated Termination Analysis of Imperative Programs (SF, DK), pp. 277–293.
CADE-2009-BorrallerasLNRR #linear #polynomial #satisfiability: Solving Non-linear Polynomial Arithmetic via SAT Modulo Linear Arithmetic (CB, SL, RNM, ERC, AR), pp. 294–305.
CADE-2009-Stickel #proving #theorem proving: Building Theorem Provers (MES), pp. 306–321.
CADE-2009-SwiderskiPGFS #analysis #dependence #induction #proving #termination #theorem proving: Termination Analysis by Dependency Pairs and Inductive Theorem Proving (SS, MP, JG, CF, PSK), pp. 322–338.
CADE-2009-KorpM #dependence #graph: Beyond Dependency Graphs (MK, AM), pp. 339–354.
CADE-2009-CiobacaDK #convergence #equation #protocol #security: Computing Knowledge in Security Protocols under Convergent Equational Theories (SC, SD, SK), pp. 355–370.
CADE-2009-EndrullisGH #complexity: Complexity of Fractran and Productivity (JE, CG, DH), pp. 371–387.
CADE-2009-ClaessenL #automation #finite #satisfiability: Automated Inference of Finite Unsatisfiability (KC, AL), pp. 388–403.
CADE-2009-HorbachW #decidability: Decidability Results for Saturation-Based Model Building (MH, CW), pp. 404–420.
CADE-2009-NguyenS #calculus #logic: A Tableau Calculus for Regular Grammar Logics with Converse (LAN, AS), pp. 421–436.
CADE-2009-GoreW #on the fly #satisfiability: An Optimal On-the-Fly Tableau-Based Decision Procedure for PDL-Satisfiability (RG, FW), pp. 437–452.
CADE-2009-MaLZ #constraints #linear: Volume Computation for Boolean Combination of Linear Arithmetic Constraints (FM, SL, JZ), pp. 453–468.
CADE-2009-BoigelotBL #automaton #theorem: A Generalization of Semenov’s Theorem to Automata over Real Numbers (BB, JB, JL), pp. 469–484.
CADE-2009-PlatzerQR #verification: Real World Verification (AP, JDQ, PR), pp. 485–501.

Renate A. SchmidtProceedings of the 22nd International Conference on Automated DeductionCADE, 2009.

Contents (35 items)

Renate A. Schmidt
Proceedings of the 22nd International Conference on Automated Deduction
CADE, 2009.