Automated Reasoning: 6th International Joint Conference, IJCAR 2012, Manchester, UK, June 26-29, 2012, Proceedings (Lecture Notes in Computer Science, 7364)

This book constitutes the refereed proceedings of the 6th International Joint Conference on Automated Reasoning, IJCAR 2012, held in Manchester, UK, in June 2012. IJCAR 2012 is a merger of leading events in automated reasoning, namely CADE (International Conference on Automated Deduction), FroCoS (International Symposium on Frontiers of Combining Systems), FTP (International Workshop on First-Order Theorem Proving), and TABLEAUX (International Conference on Automated Reasoning with Analytic Tableaux and Related Methods). The 32 revised full research papers and 9 system descriptions presented together with 3 invited talks were carefully reviewed and selected from 116 submissions. The papers address all aspects of automated reasoning, including foundations, implementations, and applications. 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}$ (Q) 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 - This book constitutes the refereed proceedings of the Third International Conference on Autonomous and Intelligent Systems, AIS 2012, held in Aveiro, Portugal, in June 2012, collocated with the International Conference on Image Analysis and Recognition, IACIAR 2012. The 31 revised full papers were carefully reviewed and selected from 48 submissions. The papers are organized in topical sections on autonomous sensors and sensor systems, autonomous systems and intelligent control with applications, intelligent fuzzy systems, intelligent robotics, intelligent knowledge management, swarm and evolutionary methods, and applications