Automated Reasoning: 6th International Joint Conference, IJCAR 2012, Manchester, UK, June 26-29, 2012. Proceedings

Front Matter....Pages -
Taking Satisfiability to the Next Level with Z3....Pages 1-8
Enlarging the Scope of Applicability of Successful Techniques for Automated Reasoning in Mathematics....Pages 9-9
SAT and SMT Are Still Resolution: Questions and Challenges....Pages 10-13
Unification Modulo Synchronous Distributivity....Pages 14-29
SAT Encoding of Unification in $\\mathcal{ELH}_{{R}^+}$ w.r.t. Cycle-Restricted Ontologies....Pages 30-44
UEL: Unification Solver for the Description Logic $\\mathcal{EL}$ – System Description....Pages 45-51
Effective Finite-Valued Semantics for Labelled Calculi....Pages 52-66
A Simplex-Based Extension of Fourier-Motzkin for Solving Linear Integer Arithmetic....Pages 67-81
How Fuzzy Is My Fuzzy Description Logic?....Pages 82-96
Truthful Monadic Abstractions....Pages 97-110
Satallax: An Automatic Higher-Order Prover....Pages 111-117
From Strong Amalgamability to Modularity of Quantifier-Free Interpolation....Pages 118-133
SPARQL Query Containment under RDFS Entailment Regime....Pages 134-148
Automated Verification of Recursive Programs with Pointers....Pages 149-163
Security Protocols, Constraint Systems, and Group Theories....Pages 164-178
Taming Past LTL and Flat Counter Systems....Pages 179-193
A Calculus for Generating Ground Explanations....Pages 194-209
EPR-Based Bounded Model Checking at Word Level....Pages 210-224
Proving Non-looping Non-termination Automatically....Pages 225-240
Rewriting Induction + Linear Arithmetic = Decision Procedure....Pages 241-255
Combination of Disjoint Theories: Beyond Decidability....Pages 256-270
Automated Analysis of Regular Algebra....Pages 271-285
 δ -Complete Decision Procedures for Satisfiability over the Reals....Pages 286-300
BDD-Based Automated Reasoning for Propositional Bi-Intuitionistic Tense Logics....Pages 301-315
From Linear Temporal Logic Properties to Rewrite Propositions....Pages 316-331
Tableaux Modulo Theories Using Superdeduction....Pages 332-338
Solving Non-linear Arithmetic....Pages 339-354
Inprocessing Rules....Pages 355-370
Logical Difference Computation with CEX2.5....Pages 371-377
Overview and Evaluation of Premise Selection Techniques for Large Theory Mathematics....Pages 378-392
Branching Time? Pruning Time!....Pages 393-407
New Algorithms for Unification Modulo One-Sided Distributivity and Its Variants....Pages 408-422
Reachability Analysis of Program Variables....Pages 423-438
Playing Hybrid Games with KeYmaera....Pages 439-453
The QMLTP Problem Library for First-Order Modal Logics....Pages 454-461
Correctness of Program Transformations as a Termination Problem....Pages 462-476
Fingerprint Indexing for Paramodulation and Rewriting....Pages 477-483
Optimization in SMT with ${\\mathcal LA}$ (ℚ) Cost Functions....Pages 484-498
Synthesis for Unbounded Bit-Vector Arithmetic....Pages 499-513
Extended Caching, Backjumping and Merging for Expressive Description Logics....Pages 514-529
KBCV – Knuth-Bendix Completion Visualizer....Pages 530-536
A PLTL-Prover Based on Labelled Superposition with Partial Model Guidance....Pages 537-543
Stratification in Logics of Definitions....Pages 544-558
Diabelli: A Heterogeneous Proof System....Pages 559-566
Back Matter....Pages -