LPAR-17 Accepted Papers

Dejan Jovanović and Clark Barrett . Polite Theories Revisited
Mark Kaminski and Gert Smolka . Clausal Graph Tableaux for Hybrid Logic with Eventualities and Difference
Jasmin Christian Blanchette and Koen Claessen. Generating Counterexamples for Structural Inductions by Exploiting Nonstandard Models
Margus Veanes , Nikolaj Bjorner and Leonardo de Moura . Symbolic Automata Constraint Solving
Camilo Rocha and José Meseguer. Constructors, Sufficient Completeness, and Deadlock Freedom of Rewrite Theories
Jean-Pierre Jouannaud and Benjamin Monate. Infinite families of finite string rewriting systems and their confluence
Roland Axelsson , Matthew Hague , Stephan Kreutzer , Martin Lange and Markus Latte . Extended Computation Tree Logic
Regis Alenda and Nicola Olivetti . Tableau calculus for the logic of comparative similarity over arbitrary distance spaces
Witold Charatonik and Piotr Witkowski . On the Complexity of the Bernays-Sch\"onfinkel Class with Datalog
Marijn Heule , Matti Järvisalo and Armin Biere . Clause Elimination Procedures for CNF Formulas
Friedrich Neurauter , Harald Zankl and Aart Middeldorp . Revisiting Matrix Interpretations for Polynomial Derivational Complexity of Term Rewriting
Jean Marie Lagniez , Gilles Audemard , Bertrand Mazure and Lakhdar Saïs . Boosting local search thanks to CDCL
Steffen Hölldobler , Norbert Manthey and Ari Saptawijaya. Improving resource-unaware SAT solvers
Laura Girodano , Valentina Gliozzi , Nicola Olivetti and Gian Luca Pozzato . A nonmonotonic extension of  KLM Preferential Logic P
Konstantin Korovin and Christoph Sticksel . Labelled Unit Superposition Calculi for Instantiation-based Reasoning
Andreas Reuss and Helmut Seidl . Bottom-up Tree Automata with Term Constraints
Franz Baader and Barbara Morawska . SAT Encoding of Unification in EL
Yuxin Deng and Rob van Glabbeek . Characterising Probabilistic Processes Logically
Kaustuv Chaudhuri . Magically Constraining the Inverse Method with Dynamic Polarity Assignment
Jerome Leroux , Daniel Kroening and Philipp Ruemmer . Interpolating Quantifier-Free Presburger Arithmetic
Theofrastos Mantadelis and Gerda Janssens . Variable Compression in ProbLog
Arnaud Fietzke , Holger Hermanns and Christoph Weidenbach . Superposition-Based Analysis of First-Order Probabilistic Timed Automata
Mutsunori Banbara , Haruki Matsunaka, Naoyuki Tamura and Katsumi Inoue . Generating Combinatorial Test Cases by Efficient SAT Encodings Suitable for CDCL SAT Solvers
Benjamin Gregoire and Jorge Luis Sacchini. Strong Normalization of the Calculus of Constructions with Type-Based Termination
Taus Brock-Nannestad and Carsten Schuermann . Focused Natural Deduction
Tino Teige and Martin Fränzle . Resolution for Stochastic Boolean Satisfiability
Guillaume Bonfante and Georg Moser . Characterising Space Complexity Classes via Knuth-Bendix Orders
Pavel Klinov , Bijan Parsia and David Picado. The Consistency of the CADIAG-2 Knowledge Base: A Probabilistic Approach
Michael Codish , Carsten Fuhs , Jürgen Giesl and Peter Schneider-Kamp . Lazy Abstraction for Size-Change Termination
Thomas Henzinger , Thibaud B. Hottelier, Laura Kovacs and Andrey Rybalchenko. Aligators for Arrays
Shahab Tasharrofi and Eugenia Ternovska . PBINT, a logic for modelling search problems involving arithmetic
Antonina Kolokolova, Yongmei Liu, David Mitchell and Eugenia Ternovska . On the Complexity of Model Expansion
Claire David , Leonid Libkin and Tony Tan. On the Satisfiability of Two-Variable Logic over Data Words
Jeremy Dawson and Rajeev Gore . Generic Methods for Formalising Sequent Calculi Applied to Provability Logic
Franz Baader , Marcel Lippmann and Hongkai Liu . Using Causal Relationships to Deal with the Ramification Problem in Action Formalisms Based on Description Logics
Petros Papapanagiotou and Jacques Fleuriot. An Isabelle-like procedural mode for HOL Light
Antti Hyvärinen, Tommi Junttila and Ilkka Niemelä . Partitioning SAT Instances for Distributed Solving
Richard McKinley. Expansion nets: Proof nets for for propositional classical logic
Mauro Ferrari , Camillo Fiorentini and Guido Fiorino. fCube:  An Efficient Prover for Intuitionistic Propositional Logic
Kai Brünnler . How to Universally Close the Existential Rule
Jean-François Condotta, Souhila Kaci , Pierre Marquis and Nicolas Schwind . A Syntactical Approach to Qualitative Constraint Networks Merging