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