Automated Reasoning

1. Front Matter

   PDF

2. Invited Papers

   1. From Reachability to Temporal Specifications in Cost-Sharing Games

      • Guy Avni, Orna Kupferman, Tami Tamir

      Pages 1-15

   2. Electronic Voting: How Logic Can Help

      • Véronique Cortier

      Pages 16-25

   3. And-Or Tableaux for Fixpoint Logics with Converse: LTL, CTL, PDL and CPDL

      • Rajeev Goré

      Pages 26-45

3. HOL

   1. Unified Classical Logic Completeness

      • Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel

      Pages 46-60

   2. A Focused Sequent Calculus for Higher-Order Logic

      • Fredrik Lindblad

      Pages 61-75

4. SAT and QBF

   1. SAT-Based Decision Procedure for Analytic Pure Sequent Calculi

      • Ori Lahav, Yoni Zohar

      Pages 76-90

   2. A Unified Proof System for QBF Preprocessing

      • Marijn J. H. Heule, Martina Seidl, Armin Biere

      Pages 91-106

   3. The Fractal Dimension of SAT Formulas

      • Carlos Ansótegui, Maria Luisa Bonet, Jesús Giráldez-Cru, Jordi Levy

      Pages 107-121

5. SMT

   1. A Gentle Non-disjoint Combination of Satisfiability Procedures

      • Paula Chocron, Pascal Fontaine, Christophe Ringeissen

      Pages 122-136

6. Equational Reasoning

   1. A Rewriting Strategy to Generate Prime Implicates in Equational Logic

      • Mnacho Echenim, Nicolas Peltier, Sophie Tourret

      Pages 137-151

   2. Finite Quantification in Hierarchic Theorem Proving

      • Peter Baumgartner, Joshua Bax, Uwe Waldmann

      Pages 152-167

   3. Computing All Implied Equalities via SMT-Based Partition Refinement

      • Josh Berdine, Nikolaj Bjørner

      Pages 168-183

   4. Proving Termination of Programs Automatically with AProVE

      • Jürgen Giesl, Marc Brockschmidt, Fabian Emmes, Florian Frohn, Carsten Fuhs, Carsten Otto et al.

      Pages 184-191

7. Verification

   1. Locality Transfer: From Constrained Axiomatizations to Reachability Predicates

      • Matthias Horbach, Viorica Sofronie-Stokkermans

      Pages 192-207

   2. Proving Termination and Memory Safety for Programs with Pointer Arithmetic

      • Thomas Ströder, Jürgen Giesl, Marc Brockschmidt, Florian Frohn, Carsten Fuhs, Jera Hensel et al.

      Pages 208-223

   3. QBF Encoding of Temporal Properties and QBF-Based Verification

      • Wenhui Zhang

      Pages 224-239

8. Proof Theory

   1. Introducing Quantified Cuts in Logic with Equality

      • Stefan Hetzl, Alexander Leitsch, Giselle Reis, Janos Tapolczai, Daniel Weller

      Pages 240-254

   2. Quati: An Automated Tool for Proving Permutation Lemmas

      • Vivek Nigam, Giselle Reis, Leonardo Lima

      Pages 255-261

   3. A History-Based Theorem Prover for Intuitionistic Propositional Logic Using Global Caching: IntHistGC System Description

      • Rajeev Goré, Jimmy Thomson, Jesse Wu

      Pages 262-268

This book constitutes the refereed proceedings of the 7th International Joint Conference on Automated Reasoning, IJCAR 2014, held as part of the Vienna Summer of Logic, VSL 2014, in Vienna, Austria, in July 2014. 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 11 system descriptions presented together with 3 invited talks were carefully reviewed and selected from 83 submissions. The papers have been organized in topical sections on HOL, SAT and QBF, SMT, equational reasoning, verification, proof theory, modal and temporal reasoning, SMT and SAT, modal logic, complexity, description logics and knowledge representation and reasoning.

• Isabelle/HOL
• description logic
• formal methods
• hybrid systems
• knowlegde representation and reasoning
• modal logic
• model checking
• ontologies
• satisfiability
• software verification
• temporal logic

• CNRS,, New York University &amp, USA

  Stéphane Demri

• Department of Computer Science, University of New Mexico, Albuquerque, USA

  Deepak Kapur

• Max Planck Institute for Informatics, Saarbrücken, Germany

  Christoph Weidenbach

Policies and ethics