BibSLEIGH — Proceedings of the Sixth International Joint Conference on Automated Reasoning

Bernhard Gramlich, Dale Miller, Uli Sattler
Proceedings of the Sixth International Joint Conference on Automated Reasoning
IJCAR, 2012.

TEST

@proceedings{IJCAR-2012,
	address       = "Manchester, England, United Kingdom",
	doi           = "10.1007/978-3-642-31365-3",
	editor        = "Bernhard Gramlich and Dale Miller and Uli Sattler",
	isbn          = "978-3-642-31364-6",
	publisher     = "{Springer International Publishing}",
	series        = "{Lecture Notes in Computer Science}",
	title         = "{Proceedings of the Sixth International Joint Conference on Automated Reasoning}",
	volume        = 7364,
	year          = 2012,
}

Contents (44 items)

IJCAR-2012-Bjorner #satisfiability: Taking Satisfiability to the Next Level with Z3 — (NB), pp. 1–8.
IJCAR-2012-Matiyasevich #automation #reasoning: Enlarging the Scope of Applicability of Successful Techniques for Automated Reasoning in Mathematics (YM), p. 9.
IJCAR-2012-Nieuwenhuis #challenge #satisfiability #smt: SAT and SMT Are Still Resolution: Questions and Challenges (RN), pp. 10–13.
IJCAR-2012-AnantharamanELNR #unification: Unification Modulo Synchronous Distributivity (SA, SE, CL, PN, MR), pp. 14–29.
IJCAR-2012-BaaderBM #encoding #ontology #satisfiability #strict #unification: SAT Encoding of Unification in ℰℒℋ_R⁺ w.r.t. Cycle-Restricted Ontologies (FB, SB, BM), pp. 30–44.
IJCAR-2012-BaaderMM #logic #named #unification: UEL: Unification Solver for the Description Logic ℰℒ — System Description (FB, JM, BM), pp. 45–51.
IJCAR-2012-BaazLZ #calculus #effectiveness #semantics: Effective Finite-Valued Semantics for Labelled Calculi (MB, OL, AZ), pp. 52–66.
IJCAR-2012-BobotCCIMMM #integer #linear: A Simplex-Based Extension of Fourier-Motzkin for Solving Linear Integer Arithmetic (FB, SC, EC, MI, AM, AM, GM), pp. 67–81.
IJCAR-2012-BorgwardtDP #fuzzy #how #logic #question: How Fuzzy Is My Fuzzy Description Logic? (SB, FD, RP), pp. 82–96.
IJCAR-2012-Brock-NannestadS #abstraction #monad: Truthful Monadic Abstractions (TBN, CS), pp. 97–110.
IJCAR-2012-Brown #automation #higher-order #named #proving: Satallax: An Automatic Higher-Order Prover (CEB), pp. 111–117.
IJCAR-2012-BruttomessoGR #composition #quantifier: From Strong Amalgamability to Modularity of Quantifier-Free Interpolation (RB, SG, SR), pp. 118–133.
IJCAR-2012-ChekolEGL #query: SPARQL Query Containment under RDFS Entailment Regime (MWC, JE, PG, NL), pp. 134–148.
IJCAR-2012-BoerBR #automation #pointer #recursion #source code #verification: Automated Verification of Recursive Programs with Pointers (FSdB, MMB, JR), pp. 149–163.
IJCAR-2012-DelauneKP #constraints #protocol #security: Security Protocols, Constraint Systems, and Group Theories (SD, SK, DP), pp. 164–178.
IJCAR-2012-DemriDS #ltl: Taming Past LTL and Flat Counter Systems (SD, AKD, AS), pp. 179–193.
IJCAR-2012-EchenimP #calculus #generative: A Calculus for Generating Ground Explanations (ME, NP), pp. 194–209.
IJCAR-2012-EmmerKKSV #bound #model checking #word: EPR-Based Bounded Model Checking at Word Level (ME, ZK, KK, CS, AV), pp. 210–224.
IJCAR-2012-EmmesEG #automation #proving: Proving Non-looping Non-termination Automatically (FE, TE, JG), pp. 225–240.
IJCAR-2012-FalkeK #induction #linear: Rewriting Induction + Linear Arithmetic = Decision Procedure (SF, DK), pp. 241–255.
IJCAR-2012-FontaineMW #decidability: Combination of Disjoint Theories: Beyond Decidability (PF, SM, CW), pp. 256–270.
IJCAR-2012-FosterS #algebra #analysis #automation: Automated Analysis of Regular Algebra (SF, GS), pp. 271–285.
IJCAR-2012-GaoAC #satisfiability: δ-Complete Decision Procedures for Satisfiability over the Reals (SG, JA, EMC), pp. 286–300.
IJCAR-2012-GoreT #automation #logic #reasoning: BDD-Based Automated Reasoning for Propositional Bi-Intuitionistic Tense Logics (RG, JT), pp. 301–315.
IJCAR-2012-HeamHK #linear #logic: From Linear Temporal Logic Properties to Rewrite Propositions (PCH, VH, OK), pp. 316–331.
IJCAR-2012-JacquelBDD #automation #deduction #modulo theories #proving #theorem proving #using #verification: Tableaux Modulo Theories Using Superdeduction — An Application to the Verification of B Proof Rules with the Zenon Automated Theorem Prover (MJ, KB, DD, CD), pp. 332–338.
IJCAR-2012-JovanovicM: Solving Non-linear Arithmetic (DJ, LMdM), pp. 339–354.
IJCAR-2012-JarvisaloHB: Inprocessing Rules (MJ, MH, AB), pp. 355–370.
IJCAR-2012-KonevLW #difference #logic: Logical Difference Computation with CEX2.5 (BK, ML, FW), pp. 371–377.
IJCAR-2012-KuhlweinLTUH #evaluation #overview #scalability: Overview and Evaluation of Premise Selection Techniques for Large Theory Mathematics (DK, TvL, ET, JU, TH), pp. 378–392.
IJCAR-2012-LatteL #branch #exclamation: Branching Time? Pruning Time! (ML, ML), pp. 393–407.
IJCAR-2012-MarshallN #algorithm #unification: New Algorithms for Unification Modulo One-Sided Distributivity and Its Variants (AMM, PN), pp. 408–422.
IJCAR-2012-NikolicS #analysis #reachability: Reachability Analysis of Program Variables (DN, FS), pp. 423–438.
IJCAR-2012-QueselP #game studies #hybrid: Playing Hybrid Games with KeYmaera (JDQ, AP), pp. 439–453.
IJCAR-2012-RathsO #first-order #library #logic #problem: The QMLTP Problem Library for First-Order Modal Logics (TR, JO), pp. 454–461.
IJCAR-2012-RauSS #correctness #problem #program transformation #termination: Correctness of Program Transformations as a Termination Problem (CR, DS, MSS), pp. 462–476.
IJCAR-2012-Schulz: Fingerprint Indexing for Paramodulation and Rewriting (SS), pp. 477–483.
IJCAR-2012-SebastianiT #cost analysis #optimisation #smt: Optimization in SMT with ℒ𝒜(ℚ) Cost Functions (RS, ST), pp. 484–498.
IJCAR-2012-SpielmannK #bound #synthesis: Synthesis for Unbounded Bit-Vector Arithmetic (AS, VK), pp. 499–513.
IJCAR-2012-SteigmillerLG #logic: Extended Caching, Backjumping and Merging for Expressive Description Logics (AS, TL, BG), pp. 514–529.
IJCAR-2012-SternagelZ #named #visualisation: KBCV — Knuth-Bendix Completion Visualizer (TS, HZ), pp. 530–536.
IJCAR-2012-SudaW: A PLTL-Prover Based on Labelled Superposition with Partial Model Guidance (MS, CW), pp. 537–543.
IJCAR-2012-Tiu #logic: Stratification in Logics of Definitions (AT), pp. 544–558.
IJCAR-2012-UrbasJ #named #proving: Diabelli: A Heterogeneous Proof System (MU, MJ), pp. 559–566.

Bernhard Gramlich, Dale Miller, Uli SattlerProceedings of the Sixth International Joint Conference on Automated ReasoningIJCAR, 2012.

Contents (44 items)

Bernhard Gramlich, Dale Miller, Uli Sattler
Proceedings of the Sixth International Joint Conference on Automated Reasoning
IJCAR, 2012.