Abstract is missing.
- Superposition and Model Evolution CombinedPeter Baumgartner, Uwe Waldmann. 17-34 [doi]
- On Deciding Satisfiability by DPLL(G+::::T::::) and Unsound Theorem ProvingMaria Paola Bonacina, Christopher Lynch, Leonardo Mendonça de Moura. 35-50 [doi]
- Combinable Extensions of Abelian GroupsEnrica Nicolini, Christophe Ringeissen, Michaël Rusinowitch. 51-66 [doi]
- Locality Results for Certain Extensions of Theories with Bridging FunctionsViorica Sofronie-Stokkermans. 67-83 [doi]
- Axiom Pinpointing in Lightweight Description Logics via Horn-SAT Encoding and Conflict AnalysisRoberto Sebastiani, Michele Vescovi. 84-99 [doi]
- Does This Set of Clauses Overlap with at Least One MUS?Éric Grégoire, Bertrand Mazure, Cédric Piette. 100-115 [doi]
- Progress in the Development of Automated Theorem Proving for Higher-Order LogicGeoff Sutcliffe, Christoph Benzmüller, Chad E. Brown, Frank Theiss. 116-130 [doi]
- System Description: H-PILoTCarsten Ihlemann, Viorica Sofronie-Stokkermans. 131-139 [doi]
- SPASS Version 3.5Christoph Weidenbach, Dilyana Dimova, Arnaud Fietzke, Rohit Kumar, Martin Suda, Patrick Wischnewski. 140-145 [doi]
- Dei: A Theorem Prover for Terms with Integer ExponentsHicham Bensaid, Ricardo Caferra, Nicolas Peltier. 146-150 [doi]
- veriT: An Open, Trustable and Efficient SMT-SolverThomas Bouton, Diego Caminha B. de Oliveira, David Déharbe, Pascal Fontaine. 151-156 [doi]
- Divvy: An ATP Meta-system Based on Axiom Relevance OrderingAlex Roederer, Yury Puzis, Geoff Sutcliffe. 157-162 [doi]
- Instantiation-Based Automated Reasoning: From Theory to PracticeKonstantin Korovin. 163-166 [doi]
- Interpolant Generation for UTVPIAlessandro Cimatti, Alberto Griggio, Roberto Sebastiani. 167-182 [doi]
- Ground Interpolation for Combined TheoriesAmit Goel, Sava Krstic, Cesare Tinelli. 183-198 [doi]
- Interpolation and Symbol EliminationLaura Kovács, Andrei Voronkov. 199-213 [doi]
- Complexity and Algorithms for Monomial and Clausal Predicate AbstractionShuvendu K. Lahiri, Shaz Qadeer. 214-229 [doi]
- Efficient Intuitionistic Theorem Proving with the Polarized Inverse MethodSean McLaughlin, Frank Pfenning. 230-244 [doi]
- A Refined Resolution Calculus for CTLLan Zhang, Ullrich Hustadt, Clare Dixon. 245-260 [doi]
- Fair Derivations in Monodic Temporal ReasoningMichel Ludwig, Ullrich Hustadt. 261-276 [doi]
- A Term Rewriting Approach to the Automated Termination Analysis of Imperative ProgramsStephan Falke, Deepak Kapur. 277-293 [doi]
- Solving Non-linear Polynomial Arithmetic via SAT Modulo Linear ArithmeticCristina Borralleras, Salvador Lucas, Rafael Navarro-Marset, Enric RodrÃguez-Carbonell, Albert Rubio. 294-305 [doi]
- Building Theorem ProversMark E. Stickel. 306-321 [doi]
- Termination Analysis by Dependency Pairs and Inductive Theorem ProvingStephan Swiderski, Michael Parting, Jürgen Giesl, Carsten Fuhs, Peter Schneider-Kamp. 322-338 [doi]
- Beyond Dependency GraphsMartin Korp, Aart Middeldorp. 339-354 [doi]
- Computing Knowledge in Security Protocols under Convergent Equational TheoriesStefan Ciobâca, Stéphanie Delaune, Steve Kremer. 355-370 [doi]
- Complexity of Fractran and ProductivityJörg Endrullis, Clemens Grabmayer, Dimitri Hendriks. 371-387 [doi]
- Automated Inference of Finite UnsatisfiabilityKoen Claessen, Ann Lillieström. 388-403 [doi]
- Decidability Results for Saturation-Based Model BuildingMatthias Horbach, Christoph Weidenbach. 404-420 [doi]
- A Tableau Calculus for Regular Grammar Logics with ConverseLinh Anh Nguyen, Andrzej Szalas. 421-436 [doi]
- An Optimal On-the-Fly Tableau-Based Decision Procedure for PDL-SatisfiabilityRajeev Goré, Florian Widmann. 437-452 [doi]
- Volume Computation for Boolean Combination of Linear Arithmetic ConstraintsFeifei Ma, Sheng Liu, Jian Zhang. 453-468 [doi]
- A Generalization of Semenov s Theorem to Automata over Real NumbersBernard Boigelot, Julien Brusten, Jérôme Leroux. 469-484 [doi]
- Real World VerificationAndré Platzer, Jan-David Quesel, Philipp Rümmer. 485-501 [doi]