Accepted Papers
Regular Papers:
- Progress in the Development of Automated Theorem Proving for Higher-order Logic
Geoff Sutcliffe, Christoph Benzmueller, Chad E. Brown and Frank Theiss - A Tableau Calculus for Regular Grammar Logics with Converse
Linh Anh Nguyen and Andrzej Szalas - Beyond Dependency Graphs
Martin Korp and Aart Middeldorp - Ground Interpolation for Theory Combination
Amit Goel, Sava Krstic and Cesare Tinelli - Superposition and Model Evolution Combined
Peter Baumgartner and Uwe Waldmann - An Optimal On-the-fly Tableau-based Decision Procedure for PDL-Satisfiability
Florian Widmann and Rajeev Gore - Does this set of clauses overlap with at least one MUS?
Eric Gregoire, Bertrand Mazure and Cedric Piette - Computing knowledge in security protocols under convergent equational theories
Stefan Ciobaca, Stephanie Delaune and Steve Kremer - Termination Analysis by Dependency Pairs and Inductive Theorem Proving
Stephan Swiderski, Michael Parting, Juergen Giesl, Carsten Fuhs and Peter Schneider-Kamp - Interpolant Generation for UTVPI
Alessandro Cimatti, Alberto Griggio and Roberto Sebastiani - Decidability Results for Saturation-Based Model Building
Matthias Horbach and Christoph Weidenbach - Efficient Intuitionistic Theorem Proving with the Polarized Inverse Method
Sean McLaughlin and Frank Pfenning - Volume Computation for Boolean Combination of Linear Arithmetic Constraints
Feifei Ma, Sheng Liu and Jian Zhang - A Generalization of Semenov's Theorem to Automata over Real Numbers
Bernard Boigelot, Julien Brusten and Jerome Leroux - A Refined Resolution Calculus for CTL
Lan Zhang, Ullrich Hustadt and Clare Dixon - Axiom Pinpointing in Lightweight Description Logics via Horn-SAT Encoding and Conflict Analysis
Roberto Sebastiani and Michele Vescovi - Combinable Extensions of Abelian Groups
Enrica Nicolini, Christophe Ringeissen and Michael Rusinowitch - Fair Derivations in Monodic Temporal Reasoning
Michel Ludwig and Ullrich Hustadt - Solving non-linear polynomial arithmetic via SAT modulo linear arithmetic
Cristina Borralleras, Salvador Lucas, Rafael Navarro-Marset, Enric Rodriguez-Carbonell and Albert Rubio - On deciding satisfiability by DPLL(Gamma+T) and unsound theorem proving
Maria Paola Bonacina, Christopher Lynch and Leonardo de Moura - Productivity is Pi^0_2-complete
Joerg Endrullis, Clemens Grabmayer and Dimitri Hendriks - Locality results for certain extensions of theories with bridging functions
Viorica Sofronie-Stokkermans - Real World Verification
Andre Platzer, Jan-David Quesel and Philipp Ruemmer - A Term Rewriting Approach to the Automated Termination Analysis of Imperative Programs
Stephan Falke and Deepak Kapur - Interpolation and Symbol Elimination
Laura Kovacs and Andrei Voronkov - Complexity and algorithms for monomial and clausal predicate abstraction
Shuvendu Lahiri and Shaz Qadeer - Automated Inference of Finite Unsatisfiability
Koen Claessen and Ann Lilliestrom
System descriptions
- Divvy: A ATP Meta-system based on Axiom Relevance Ordering
Alexander Roederer, Yury Puzis and Geoff Sutcliffe - DEI: A Theorem Prover for Terms with Integer Exponents
Hicham Bensaid, Ricardo Caferra and Nicolas Peltier - veriT: an open, trustable and efficient SMT-solver
Thomas Bouton, Diego Caminha B. de Oliveira, David Deharbe and Pascal Fontaine - SPASS Version 3.5
Christoph Weidenbach, Arnaud Fietzke, Rohit Kumar, Martin Suda, Patrick Wischnewski and Dilyana Dimova - System Description: H-PILoT Version 1.5
Carsten Ihlemann and Viorica Sofronie-Stokkermans
