Automated Reasoning: 8th International Joint Conference, IJCAR 2016, Coimbra, Portugal, June 27 – July 2, 2016, Proceedings (Lecture Notes in Computer Science Book 9706)

This book constitutes the refereed proceedings of the 8th International Joint Conference on Automated Reasoning, IJCAR 2016, held in Coimbra, Portugal, in June/July 2016. IJCAR 2014 was a merger of three leading events in automated reasoning, namely CADE (International Conference on Automated Deduction), FroCoS (International Symposium on Frontiers of Combining Systems) and TABLEAUX (International Conference on Automated Reasoning with Analytic Tableaux and Related Methods). The 26 revised full research papers and 9 system descriptions presented together with 4 invited talks were carefully reviewed and selected from 79 submissions. The papers have been organized in topical sections on satisfiability of Boolean formulas, satisfiability modulo theory, rewriting, arithmetic reasoning and mechanizing mathematics, first-order logic and proof theory, first-order theorem proving, higher-order theorem proving, modal and temporal logics, non-classical logics, and verification. Front Matter....Pages I-XX Front Matter....Pages 1-1 A Logical Framework for Developing and Mechanizing Set Theories....Pages 3-8 Programming by Examples: Applications, Algorithms, and Ambiguity Resolution....Pages 9-14 Logic & Proofs for Cyber-Physical Systems....Pages 15-21 Front Matter....Pages 23-23 A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality....Pages 25-44 Super-Blocked Clauses....Pages 45-61 Front Matter....Pages 63-63 Counting Constraints in Flat Array Fragments....Pages 65-81 A New Decision Procedure for Finite Sets and Cardinality Constraints in SMT....Pages 82-98 Congruence Closure in Intensional Type Theory....Pages 99-115 Fast Cube Tests for LIA Constraint Solving....Pages 116-132 Model Finding for Recursive Functions in SMT....Pages 133-151 Colors Make Theories Hard....Pages 152-170 Front Matter....Pages 171-171 Nominal Confluence Tool....Pages 173-182 Built-in Variant Generation and Unification, and Their Applications in Maude 2.7....Pages 183-192 Front Matter....Pages 193-193 Race Against the Teens – Benchmarking Mechanized Math on Pre-university Problems....Pages 195-212 raSAT: An SMT Solver for Polynomial Constraints....Pages 213-227 Front Matter....Pages 228-237 Schematic Cut Elimination and the Ordered Pigeonhole Principle ....Pages 239-239 Subsumption Algorithms for Three-Valued Geometric Resolution....Pages 241-256 On Interpolation and Symbol Elimination in Theory Extensions....Pages 257-272 Front Matter....Pages 273-289 System Description: GAPT 2.0....Pages 291-291 Front Matter....Pages 293-301 Selecting the Selection....Pages 291-291 Performance of Clause Selection Heuristics for Saturation-Based Theorem Proving....Pages 302-312 Front Matter....Pages 313-329 Internal Guidance for Satallax....Pages 330-345 Effective Normalization Techniques for HOL....Pages 347-347 Front Matter....Pages 349-361 Complexity Optimal Decision Procedure for a Propositional Dynamic Logic with Parallel Composition....Pages 362-370 Interval Temporal Logic Model Checking: The Border Between Good and Bad HS Fragments....Pages 371-371 Inducing Syntactic Cut-Elimination for Indexed Nested Sequents....Pages 373-388 Front Matter....Pages 389-405 A Tableau System for Quasi-Hybrid Logic....Pages 406-415 Machine-Checked Interpolation Theorems for Substructural Logics Using Display Calculi....Pages 416-432 Intuitionistic Layered Graph Logic....Pages 433-433 Gen2sat: An Automated Tool for Deciding Derivability in Analytic Pure Sequent Calculi....Pages 435-451 Front Matter....Pages 452-468 Model Checking Parameterised Multi-token Systems via the Composition Method....Pages 469-486 Unbounded-Thread Program Verification using Thread-State Equations....Pages 487-495 A Complete Decision Procedure for Linearly Compositional Separation Logic with Data Constraints....Pages 497-497 Lower Runtime Bounds for Integer Programs....Pages 499-515 Translating Scala Programs to Isabelle/HOL....Pages 516-531 Back Matter....Pages 532-549 ....Pages 550-567