LPAR-17 Accepted Papers with Abstracts

Dejan Jovanović and Clark Barrett . Polite Theories Revisited
Abstract: The classic method of Nelson and Oppen for combining decision procedures requires the theories to be stably-infinite. Unfortunately, some important theories do not fall into this category (e.g. the theory of bit-vectors). To remedy this problem, previous work introduced the notion of polite theories. Polite theories can be combined with any other theory using an extension of the Nelson-Oppen approach. In this paper we revisit the notion of polite theories, fixing a subtle flaw in the original definition. We give a new combination theorem which specifies the degree to which politeness is preserved when combining polite theories. We also give conditions under which politeness is preserved when instantiating theories by identifying two sorts. These results lead to a more general variant of the theorem for combining multiple polite theories.
Mark Kaminski and Gert Smolka . Clausal Graph Tableaux for Hybrid Logic with Eventualities and Difference
Abstract: We introduce the method of clausal graph tableaux at the example of hybrid logic with difference and star modalities.  Clausal graph tableaux are prefix-free and terminate by construction.  They provide an abstract method of establishing the small model property of modal logics.  In contrast to the filtration method, clausal graph tableaux result in goal-directed decision procedures.  Until now no goal-directed decision procedure for the logic considered in this paper was known.  There is the promise that clausal graph tableaux lead to a new class of effective decision procedures.
Jasmin Christian Blanchette and Koen Claessen. Generating Counterexamples for Structural Inductions by Exploiting Nonstandard Models
Abstract: Induction proofs often fail because the stated theorem is non-inductive, in which case the user must strengthen the theorem or prove auxiliary properties before performing the induction step. (Counter)model finders are useful for detecting non-theorems, but they will not find any counterexamples for non-inductive theorems. We explain how to apply a well-known concept from first-order logic, nonstandard models, to the detection of non-inductive invariants. Our work was done in the context of the proof assistant Isabelle/HOL and the counterexample generator Nitpick.
Margus Veanes , Nikolaj Bjorner and Leonardo de Moura . Symbolic Automata Constraint Solving
Abstract: Constraints over regular and context-free languages are common in the context of string-manipulating programs. Efficient solving of such constraints, often in combination with arithmetic and other theories, has many useful applications in program analysis and testing. We introduce and evaluate a method for symbolically expressing and solving constraints over automata, including subset constraints. Our method uses techniques present in the state-of-the-art SMT solver Z3.
Camilo Rocha and José Meseguer. Constructors, Sufficient Completeness, and Deadlock Freedom of Rewrite Theories
Abstract: Sufficient completeness has been throughly studied for equational specifications $(\Sigma,E)$, where function symbols are classified into {\em constructors} and {\em defined} symbols. But what should sufficient completeness mean for a rewrite theory $\mathcal{R} = (\Sigma,E,R)$ with equations $E$ and non-equational rules $R$ describing concurrent transitions in a system? This work argues that a rewrite theory naturally has {\em two} notions of constructor: the usual one for its equations $E$, and a different  one for its rules $R$. The sufficient completeness of constructors for the rules $R$ turns out to be intimately related with \emph{deadlock freedom}, i.e., $\mathcal{R}$ has no deadlocks outside the constructors for $R$. The relation between these two notions is studied in the setting of unconditional order-sorted rewrite theories. Sufficient conditions are given allowing the automatic checking of sufficient completeness, and other related properties, by equational tree automata modulo equational axioms such as associativity, commutativity, and identity. They are used to extend the Maude Sufficient Completeness Checker from the checking of equational theories to that of both equational and rewrite theories.  Finally, the usefulness of the proposed notion of constructors in proving inductive theorems about the reachability rewrite relation $\rightarrow_\mathcal{R}$ associated to a rewrite theory $\mathcal{R}$ (and also about the joinability relation $\downarrow_\mathcal{R}$) is both characterized and illustrated with examples.
Jean-Pierre Jouannaud and Benjamin Monate. Infinite families of finite string rewriting systems and their confluence
Abstract: We introduce parameterized rewrite systems for describing infinite families of finite string rewrite systems depending upon non-negative integer parameters, as well as ways to reason uniformly over these families. Unlike previous work, the vocabulary on which a rewrite system in the family is built depends itself on the integer parameters. Rewriting makes use of a toolkit for parameterized words which allows to describe a rewrite step made independently by all systems in an infinite family by a single, effective parameterized rewrite step. The main result is a confluence test for all systems in a family at once, based on a critical pair lemma classically based on computing (finitely many) overlaps between lefthand sides of parameterized rules and then checking for their joinability. A termination test for all systems in the family is also described.
Roland Axelsson , Matthew Hague , Stephan Kreutzer , Martin Lange and Markus Latte . Extended Computation Tree Logic
Abstract: We introduce a generic extension of the popular branching-time logic CTL which refines the temporal until and release operators with formal languages.  For instance, a language may determine the moments along a path that an until property may be fulfilled.  We consider several classes of languages leading to logics with different expressive power and complexity,  whose importance is motivated by their use in model checking, synthesis, abstract interpretation, etc.  

We show that even with context-free languages on the until operator the logic still allows for polynomial time model-checking despite the significant increase in expressive power. This makes the logic a promising candidate for applications in verification.  

In addition, we analyse the complexity of satisfiability and compare the expressive power of these logics to CTL* and extensions of PDL.
Regis Alenda and Nicola Olivetti . Tableau calculus for the logic of comparative similarity over arbitrary distance spaces
Abstract: The logic CSL (first introduced by Sheremet, Tishkowsky, Wolter and Zakharyaschev  in 2005)  allows one to reason about distance comparison and  similarity comparison within a modal language. The logic can express assertions of the kind "A is closer/more similar to B than to C" and has a natural application to spatial reasoning, as well as to reasoning about concept similarity in ontologies. The semantics of CSL is defined in terms of models based on different classes of distance spaces and it generalizes  the logic S4u of topological spaces.  In this paper we consider CSL defined over arbitrary distance spaces. The logic comprises a binary modality  to represent comparative similarity and a unary  modality to express the existence of the minimum of a set of distances.  We first show that the semantics of CSL can be equivalently defined in terms of preferential models. As a consequence we obtain the finite model property of the logic with respect to its preferential semantic, a property that does not hold with respect to the original distance-space semantics. Next we present an analytic tableau calculus based on its preferential semantics.
The calculus provides a decision procedure for the logic, its termination is obtained by imposing suitable blocking restrictions.
Witold Charatonik and Piotr Witkowski . On the Complexity of the Bernays-Sch\"onfinkel Class with Datalog
Abstract: Bernays-Sch\"onfinkel class with Datalog is a 2-variable fragment of
the Bernays-Sch\"onfinkel class extended with least fixed points
expressible by certain monadic Datalog programs. It was used in a
bounded model checking procedure for programs manipulating dynamically
allocated pointer structures, where the bounded model checking problem
was reduced to the satisfiability of formulas in this logic. The
best known upper bound on the complexity of the satisfiability problem
for this logic was 2NEXPTIME.

In this paper we establish the complexity of the satisfiability
problem of Bernays-Sch\"onfinkel class with Datalog. We prove
NEXPTIME-completeness of the problem by showing an appropriate lower
bound and proposing a new algorithm running in NEXPTIME. Our algorithm
is based on a translation to 2-variable logic with counting
quantifiers. As a by-product we obtain that the extension of
Bernays-Sch\"onfinkel class with Datalog to 2-variable logic with
counting and Datalog is decidable without increase of complexity.  We
also solve the entailment problem for this logic, which in some
situations gives us an extension of the bounded model checking
procedure to a verification method.
Marijn Heule , Matti Järvisalo and Armin Biere . Clause Elimination Procedures for CNF Formulas
Abstract: This paper develops and analyzes clause elimination procedures, a
specific family of simplification techniques for conjunctive normal
form (CNF) formulas. In addition to considering existing procedures
such as tautology, subsumption , and blocked clause elimination, we
introduce novel elimination procedures based on hidden and asymmetric
variants of these techniques. We analyze the resulting nine (including
four formerly introduced and five new) satisfiability-preserving
clause elimination procedures from various perspectives: size
reduction, BCP-preservance, confluence, and logical equivalence.
Furthermore, for the variants that do not preserve logical
equivalence, we show how to reconstruct solutions to original CNFs
from satisfying assignments to simplified CNFs. We also include an
experimental evaluation on the effectiveness of selected procedures.
Friedrich Neurauter , Harald Zankl and Aart Middeldorp . Revisiting Matrix Interpretations for Polynomial Derivational Complexity of Term Rewriting
Abstract: Matrix interpretations can be used to bound the derivational complexity of
term rewrite systems. In particular, triangular matrix interpretations
over the natural numbers are known to induce polynomial upper bounds
on the derivational complexity of (compatible) rewrite systems.
Using techniques from linear algebra, we show how one can generalize the
method to matrices that are not necessarily triangular but nevertheless
polynomially bounded.
Moreover, we show that our approach also applies to matrix interpretations
over the real (algebraic) numbers. In particular, it includes a refinement
of triangular matrix interpretations as a special case, which allows to
infer tighter bounds than the original approach.
Jean Marie Lagniez , Gilles Audemard , Bertrand Mazure and Lakhdar Saïs . Boosting local search thanks to CDCL
Abstract: In this paper, a novel hybrid and complete approach for propositional
satisfiability, called SatHyS (Sat Hybrid Solver), is introduced. It efficiently
combines the strength of both local search and CDCL based SAT solvers. Con-
sidering the consistent partial assignment under construction by the CDCL SAT
solver, local search is used to extend it to a model of the Boolean formula, while
the CDCL component is used by the local search one as a strategy to escape from
a local minimum. Additionally, both solvers heavily cooperate thanks to relevant
information gathered during search. Experimentations on SAT instances taken
from the last competitions demonstrate the efficiency and the robustness of our
hybrid solver with respect to the state-of-the-art CDCL based, local search and
hybrid SAT solvers.
Steffen Hölldobler , Norbert Manthey and Ari Saptawijaya. Improving resource-unaware SAT solvers
Abstract: The paper discusses cache utilization in state-of-the-art SAT
solvers. The aim of the study is to show how a resource-unaware SAT
solver can be improved by utilizing the cache sensibly. The analysis is
performed on a CDCL-based SAT solver using a subset of the indus-
trial SAT Competition 2009 benchmark. For the analysis, the total cy-
cles, the resource stall cycles, the L2 cache hits and the L2 cache misses
are traced using sample based profiling. Based on the analysis, several
techniques – some of which have not been used in SAT solvers so far – are
proposed resulting in a combined speedup up to 83% without affecting
the search path of the solver. The average speedup on the benchmark is
60%. The new techniques are also applied to MiniSAT 2.0 improving its
runtime by 20% on average.
Laura Girodano , Valentina Gliozzi , Nicola Olivetti and Gian Luca Pozzato . A nonmonotonic extension of  KLM Preferential Logic P
Abstract: In this paper, we propose the logic Pmin , which is a non-
monotonic extension of Preferential logic P defined by Kraus, Lehmann
and Magidor (KLM). In order to perform nonmonotonic inferences, we
define a “minimal model” semantics. Given a modal interpretation of a
minimal A-world as A ∧ 􏰁¬A, the intuition is that preferred, or mini-
mal models are those that minimize the number of worlds where ¬􏰁¬A
holds, that is of A- worlds which are not minimal. We present a tableau
calculus for deciding entailment in Pmin.
Konstantin Korovin and Christoph Sticksel . Labelled Unit Superposition Calculi for Instantiation-based Reasoning
Abstract: The Inst-Gen-Eq method is an instantiation-based calculus which is complete for first-order clause logic modulo equality. Its distinctive feature is that it combines first-order reasoning with efficient ground satisfiability checking which is delegated in a modular way to any state-of-the-art ground SMT solver.

The first-order reasoning employs a superposition-style calculus which generates the instances needed by the ground solver to refine a model of an abstraction or to witness unsatisfiability.

In this paper we present and compare different labelling mechanisms in the unit superposition calculus that facilitates finding the necessary instances. We demonstrate and evaluate how different label structures such as sets or AND/OR trees affect the interplay between the proof procedure and blocking mechanisms for redundancy elimination.
Andreas Reuss and Helmut Seidl . Bottom-up Tree Automata with Term Constraints
Abstract: We introduce bottom-up tree automata with equality and disequality term constraints. These constraints are more expressive than the equality and disequality constraints between brothers introduced by Bogaert and Tison in 1992. Our new class of automata is still closed under Boolean operations. Moreover, we show that for tree automata with term constraints not only membership but also emptiness is decidable. This contrasts with the undecidability of emptiness for automata with arbitrary equality constraints between subterms identified by paths as shown in 1981 by Mongy.
Franz Baader and Barbara Morawska . SAT Encoding of Unification in EL
Abstract: Unification in Description Logics has been proposed as a novel inference service that can, for example, be used to detect redundancies in ontologies. In a recent paper, we have shown that unification in the Description Logic EL is NP-complete, and thus of a complexity that is considerably lower than in other Description Logics of comparably restricted expressive power.

In this paper, we introduce a new NP-algorithm for solving unification problems in EL, which is based on a reduction to satisfiability in propositional logic (SAT). The advantage of this new algorithm is, on the one hand, that it allows us to employ highly optimized state of the art SAT solvers when implementing an EL-unification algorithm. On the other hand, this reduction provides us with a proof of the fact that EL-unification is in NP that is much simpler than the one given in our previous paper on EL-unification.
Yuxin Deng and Rob van Glabbeek . Characterising Probabilistic Processes Logically
Abstract: In this paper we work on (bi)simulation semantics of processes that
exhibit both nondeterministic and probabilistic behaviour.
We propose a probabilistic extension of the modal mu-calculus and show
how to derive characteristic formulae for various simulation-like
preorders over finite-state processes without divergence.
In addition, we show that even without the fixpoint operators
this probabilistic mu-calculus can be used to characterise these
behavioural relations in the sense that two states are equivalent
if and only if they satisfy the same set of formulae.
Kaustuv Chaudhuri . Magically Constraining the Inverse Method with Dynamic Polarity Assignment
Abstract: Given a logic program that is terminating and mode-correct in an idealised Prolog interpreter (i.e., in a top-down logic programming engine), a bottom-up logic programming engine can be used to compute exactly the same set of answers as a top-down engine for a given mode-correct query, but this requires rewriting the program and the query using, for example, the Magic Set Transform (MST). In previous work, we have shown that the focusing can realize the standard notion of bottom-up logic programming if atomic formulas are statically given a certain polarity assignment. In an analogous manner, we show here that dynamically assigning polarities can realize the effect of MST in the inverse method, without needing to rewrite the program or the query. This gives us a new proof of the compleness of MST in purely logical terms, by using the general completeness theorem for focusing. We also discuss general completeness criteria for arbitrary dynamic polarity assignment strategies.
Jerome Leroux , Daniel Kroening and Philipp Ruemmer . Interpolating Quantifier-Free Presburger Arithmetic
Abstract: Craig interpolation has become a key ingredient in many symbolic
model checkers, serving as an approximative replacement for
expensive quantifier elimination. In this paper, we focus on an
interpolating decision procedure for the full quantifier-free
fragment of Presburger Arithmetic, i.e., linear arithmetic
over the integers, a theory which is a good fit for the analysis of
software systems. In contrast to earlier procedures based on
quantifier elimination and the Omega test, our approach uses integer
linear programming techniques: relaxation of interpolation problems
to the rationals, and a complete branch-and-bound rule tailored to
efficient interpolation. Equations are handled via a dedicated
polynomial-time sub-procedure. We have fully implemented our
procedure on top of the SMT-solver OpenSMT and present an extensive
experimental evaluation.
Theofrastos Mantadelis and Gerda Janssens . Variable Compression in ProbLog
Abstract: In order to compute the probability of a query, ProbLog represents the proofs of the query as disjunctions of conjuctions, for which a Reduced Ordered Binary Decision Diagram (ROBDD) is computed. The paper identifies patterns of Boolean variables that occur in Boolean formulae, namely AND-clusters and OR-clusters. Our method compresses the variables in these clusters and thus reduces the size of ROBDDs without affecting the probability.

We give a polynomial algorithm that detects AND-clusters in disjunctive normal form (DNF) Boolean formulae, or OR-clusters in conjunctive normal form (CNF) Boolean formulae.

We do an experimental evaluation of the effects of AND-cluster compression for a real application of ProbLog. With our prototype implementation we have a significant improvement in performance (up to 87\%) for the generation of ROBDDs. Moreover, compressing AND-clusters of Boolean variables in the DNFs makes it feasible to deal with ProbLog queries that give rise to larger DNFs.
Arnaud Fietzke , Holger Hermanns and Christoph Weidenbach . Superposition-Based Analysis of First-Order Probabilistic Timed Automata
Abstract: This paper discusses the analysis of first-order probabilistic timed automata (FPTA)
by a combination of hierarchic first-order superposition-based
theorem proving and probabilistic model checking.
We develop the overall semantics of FPTAs and prove soundness and completeness
of our method for reachability properties.
Basically, we decompose FPTAs into their time plus first-order logic aspects on the one hand,
and their probabilistic aspects on the other hand. Then we exploit the time plus first-order behavior
by hierarchic superposition over linear arithmetic. The result of this analysis is
the basis for the construction of a reachability equivalent (to the original FPTA) probabilistic timed automaton
to which probabilistic model checking is finally applied.
Even though we are facing first-order undecidability and the combination of first-order
logic and linear arithmetic is not compact nor complete in general,
for the proposed FPTA it even works nice in practice. We illustrate the potential behind it with
a real-life DHCP protocol example, which we analyze by means of prototypical tool support.
Mutsunori Banbara , Haruki Matsunaka, Naoyuki Tamura and Katsumi Inoue . Generating Combinatorial Test Cases by Efficient SAT Encodings Suitable for CDCL SAT Solvers
Abstract: Generating test cases for combinatorial testing is to find a covering
array in Combinatorial Designs.
In this paper, we consider the problem of finding optimal covering
arrays by SAT encoding.
We present two encodings suitable for modern CDCL SAT solvers.
One is based on the order encoding that is efficient in the sense that
unit propagation achieves the bounds consistency in CSPs.
Another one is based on a combination of the order encoding and
Hnich's encoding.
CDCL SAT solvers have an important role in the latest SAT technology.
The effective use of them is essential for enhancing efficiency.
In our experiments, we found solutions that can be competitive with
the previously known results for the arrays of strength two to six
with small to moderate size of components and symbols.
Moreover, we succeeded either in proving the optimality of known
bounds or in improving known lower bounds for some arrays.
Benjamin Gregoire and Jorge Luis Sacchini. Strong Normalization of the Calculus of Constructions with Type-Based Termination
Abstract: Termination of recursive functions is an important property in proof assistants based on dependent type theories; it implies consistency and decidability of type checking. Type-based termination is a mechanism for ensuring termination that uses types annotated with size information to check that recursive calls are performed on smaller arguments. Our long-term goal is to extend the Calculus of Inductive Constructions with a type-based termination mechanism and prove its logical consistency. In this paper, we present an extension of the Calculus of Constructions (including universes and impredicativity) with sized natural numbers, and prove strong normalization and logical consistency. Moreover, the proof can be easily adapted to include other inductive types.
Taus Brock-Nannestad and Carsten Schuermann . Focused Natural Deduction
Abstract: Natural deduction for intuitionistic linear logic is known to be
  full of non-deterministic choices.  In order to control these
  choices, we combine ideas from intercalation and focusing to arrive
  at the calculus of \emph{focused natural deduction}.  The
  calculus is shown to be sound and complete.
Tino Teige and Martin Fränzle . Resolution for Stochastic Boolean Satisfiability
Abstract: The stochastic Boolean satisfiability (SSAT) problem was introduced by Papadimitriou in 1985 by adding a probabilistic model of uncertainty to propositional satisfiability through randomized quantification. SSAT has many applications, e.g., in probabilistic planning and, more recently by integrating arithmetic, in probabilistic model checking.
In this paper, we first present a new result on the computational complexity of SSAT: SSAT remains PSPACE-complete even for its restriction to 2CNF. Second, we propose a sound and complete resolution calculus for SSAT complementing the classical backtracking search algorithms.
Guillaume Bonfante and Georg Moser . Characterising Space Complexity Classes via Knuth-Bendix Orders
Abstract: In this paper we study three different space complexity
classes: LINSPACE, PSPACE, and ESPACE, which are commonly
believed to be distinct. We give complete characterisations of these
classes exploiting rewrite systems, whose termination can be
shown by Knuth-Bendix orders. To capture LINSPACE, we consider
positively weighted systems. To capture PSPACE, we consider unary
rewrite systems, where we allow for padding of the input. And to
capture ESPACE, we make use of a variant of the
Knuth-Bendix order, induced by quasi-precedences.
Pavel Klinov , Bijan Parsia and David Picado. The Consistency of the CADIAG-2 Knowledge Base: A Probabilistic Approach
Abstract: This paper presents the methodology and the results of checking consistency of a large-scale medical expert system CADIAG-2. The system includes a knowledge base that contains a large collection of rules representing knowledge about various symptoms, diseases and relationships between them. The major portion of the rules are uncertain, i.e. they specify to what degree a disease is confirmed by a symptom. Given the size of the system and the uncertainty it has been challenging to validate its consistency. Recent attempts to formalize CADIAG-2's knowledge base into decidable Godel logics have shown that, on that formalization, CADIAG-2 is inconsistent. In this paper we verify this result with an alternative formalization of CADIAG-2 as a set of probabilistic formulas and apply a state-of-the-art probabilistic logic solver to determine the satisfiability and extract conflict sets. As CADIAG-2 is too large to be handled out of the box, we describe an approach to split knowledge base into fragments that can be tested independently and prove that such methodology is complete, i.e. is guaranteed to find all inconsistencies. With this approach, we are able to determine that CADIAG-2 contains
numerous sets of conflicting rules and compute all of them for its slightly relaxed version.
Michael Codish , Carsten Fuhs , Jürgen Giesl and Peter Schneider-Kamp . Lazy Abstraction for Size-Change Termination
Abstract: Size-change termination is a widely used means of proving termination where source programs are first abstracted to size-change graphs which are then analyzed to determine if they satisfy the size-change termination property. Here, the choice of the abstraction is crucial to the success of the method, and it is an open problem how to choose an abstraction such that no critical loss of precision occurs. This paper shows how to couple the search for a suitable abstraction and the test for size-change termination via an encoding to a single SAT instance. In this way, the problem of choosing the right abstraction is solved en passant by a SAT solver. We show that for the setting of term rewriting, the integration of this approach into the dependency pair framework works smoothly and gives rise to a new class of size-change reduction pairs. We implemented size-change reduction pairs in the termination prover AProVE and evaluated their usefulness in extensive experiments.
Thomas Henzinger , Thibaud B. Hottelier, Laura Kovacs and Andrey Rybalchenko. Aligators for Arrays
Abstract: This tool paper describes how universally quantified array invariants
are generated with the software package Aligators. Our approach leverages recurrence
solving and algebraic techniques to carry inductive reasoning over array
content. We have successfully applied Aligators to a large number of examples.
Our experimental results give practical justification for the efficiency and applicability of our tool.
Shahab Tasharrofi and Eugenia Ternovska . PBINT, a logic for modelling search problems involving arithmetic
Abstract: Motivated by computer science challenges, Gradel and Gurevich [GG98] suggested
to extend the approach and methods of finite model theory beyond finite
structures, an approach they called Metafinite Model Theory. We develop this
direction further, in application to constraint specification/modelling
languages. Following [TM09], we use a framework based on embedded model theory,
but with a different background structure, the structure of arithmetic which
contains at least (N; 0, 1, +, ×, <, || ||), where ||x|| returns the size of the
binary encoding of x. We prove that on these structures, we can unconditionally
capture NP using a variant of a guarded logic. This improves the result of
[TM09] (and thus indirectly [GG98]) by eliminating the small cost condition on
input structures.

As a consequence, our logic (an idealized specification language) allows one to
represent common arithmetical problems such as integer factorization or disjoint
scheduling naturally, with “built-in” arithmetic, as opposed to using a binary
encoding. Thus, this result gives a remedy to a problem with practical
specification languages, namely that there are common arithmetical problems that
can be decided in NP but cannot be axiomatized naturally in current modelling
languages. We give some examples of such axiomatizations in PBINT and explain
how our result applies to constraint specification/modelling languages.
Antonina Kolokolova, Yongmei Liu, David Mitchell and Eugenia Ternovska . On the Complexity of Model Expansion
Abstract: We aim at developing theoretical foundations
of languages for representing and solving combinatorial search problems.
We consider the model expansion  (MX) task, i.e.,
the problem of expanding a given finite structure
with additional relations to produce a finite model of a formula.
This is the logical task underlying a number of practical constraint-based
systems.  We study the complexity of MX for several fragments and
extensions of FO that are promising for constraint modelling  languages, in particular,
for a guarded fragment GF_k of FO and for extensions of FO and GF_k
with inductive definitions. We analyze MX (for each of the languages)
in the context of two other  related
tasks -- model checking (the entire
structure is given) and finite satisfiability (no structure is given).
We look at both data and combined complexity.
Our main results are about the logics above.
In addition, we summarize many previously known facts
for several related logics and provide many  consequences of known
results to complete the picture. While these consequences are often not
very hard, having a complete picture is very useful and has never been
done before.
Claire David , Leonid Libkin and Tony Tan. On the Satisfiability of Two-Variable Logic over Data Words
Abstract: Data trees and data words have been studied extensively in connection with XML reasoning. These are trees or words that, in addition to labels from a finite alphabet, carry labels from an infinite alphabet (data). While in general logics such as MSO or FO are undecidable for such extensions, decidablity results for their fragments have been obtained recently, most notably for the two-variable fragments of FO and existential MSO. The proofs, however, are very long and nontrivial, and some of them come with no complexity guarantees. Here we give a much simplified proof of the decidability of two-variable logics for data words with the successor and data-equality predicates. In addition, the new proof provides several new fragments of lower complexity. The proof mixes database-inspired  constraints with encodings in Presburger arithmetic.
Jeremy Dawson and Rajeev Gore . Generic Methods for Formalising Sequent Calculi Applied to Provability Logic
Abstract: We describe generic methods for reasoning about multiset-based
  sequent calculi which allow
  us to combine shallow and deep embeddings as desired.  Our methods
  are modular, permit explicit structural rules, and are widely
  applicable to many sequent systems, even to other styles of calculi
  like natural deduction and term rewriting systems.
  We describe new axiomatic type classes
  which enable simplification of multiset or sequent expressions using
  existing algebraic manipulation facilities. We demonstrate the
  benefits of our combined approach by formalising in Isabelle/HOL a
  variant of a recent, non-trivial, pen-and-paper proof of
  cut-admissibility for the provability logic GL,
  where we express a large part of the proof in a way which is
  immediately applicable to other logics.
  Our work also provides a machine-checked proof to settle the controversy
  surrounding the proof of cut-admissibility for GL.
Franz Baader , Marcel Lippmann and Hongkai Liu . Using Causal Relationships to Deal with the Ramification Problem in Action Formalisms Based on Description Logics
Abstract: In the reasoning about actions community, causal relationships have been proposed
as a possible approach for solving the ramification problem, i.e., the problem
of how to deal with indirect effects of actions. In this paper, we show that
causal relationships can be added to action formalisms based on Description Logics
without destroying the decidability of the consistency and the projection problem.
We investigate the complexity of these decision problems based on which description logic is used as base logic for the action formalism.
Petros Papapanagiotou and Jacques Fleuriot. An Isabelle-like procedural mode for HOL Light
Abstract: HOL Light is a modern theorem proving system characterised by its powerful, low level interface that allows for flexibility and programmability. However, considerable effort is required to become accustomed to the system and to reach a point where one can comfortably achieve simple natural deduction proofs. Isabelle is another powerful and widely used theorem prover that provides useful features for natural deduction proofs, including its meta-logic and its four main natural deduction tactics. In this paper we describe our efforts to emulate some of these features of Isabelle in HOL Light. One of our aims is to decrease the learning curve of HOL Light and make it more accessible and usable by a range of users, while preserving its programmability.
Antti Hyvärinen, Tommi Junttila and Ilkka Niemelä . Partitioning SAT Instances for Distributed Solving
Abstract: In this paper we study the problem of solving hard propositional
satisfiability problem (SAT) instances in a computing grid or cloud,
where run times and communication between parallel running computations
are limited.
We study analytically an approach where the instance is partitioned
iteratively into a tree of subproblems and each node in the tree is
solved in parallel.
We present new methods for constructing partitions which combine clause
learning and look-ahead.  The methods are incorporated into the iterative approach and its
performance is demonstrated with an extensive comparison against
the best sequential solvers as well as against the best parallelsolver in the SAT competition 2009.
Richard McKinley. Expansion nets: Proof nets for for propositional classical logic
Abstract: We give a calculus of proof-nets for classical propositional logic. These nets improve on a proposal due to Robinson by validating the associativity and commutativity of contraction, and provide canonical representants for classical sequent proofs modulo natural equivalences. We present the relationship between sequent proofs and proof-nets as an annotated sequent calculus, deriving formulae decorated with terms called expansion/deletion trees. We then see a subcalculus, expansion nets, which in addition to these good properties has a polynomial-time correctness criterion. Expansion trees for first-order logic give a structured version of Herbrand’s theorem; similarly, expansion/deletion trees give a connec- tion between classical provability and provability in MLL
Mauro Ferrari , Camillo Fiorentini and Guido Fiorino. fCube:  An Efficient Prover for Intuitionistic Propositional Logic
Abstract: In this system description we provide fCube, a theorem prover for Intuitionistic
propositional logic based on a tableau calculus. The main novelty of  fCube is
that it implements several optimization techniques that allow to prune the
search space acting on different aspects of the proof-search. We tested the
efficiency of our techniques by comparing fCube with other theorem
provers. We found that our prover outperforms the other provers on several
interesting families of formulas.
Kai Brünnler . How to Universally Close the Existential Rule
Abstract: This paper introduces a nested sequent system for predicate logic.
The system features a structural universal quantifier and a
universally closed existential rule. One nice consequence of this is
that proofs of sentences cannot contain free variables.  Another
nice consequence is that the assumption of a non-empty domain is
isolated in a single inference rule. This rule can be removed or
added at will, leading to a system for free logic or classical
predicate logic, respectively. The system for free logic is
interesting because it has no need for an existence predicate. We
see syntactic cut-elimination and completeness results for these two
systems as well as two standard applications: Herbrand's Theorem and
interpolation.
Jean-François Condotta, Souhila Kaci , Pierre Marquis and Nicolas Schwind . A Syntactical Approach to Qualitative Constraint Networks Merging
Abstract: We address the problem of merging qualitative constraint networks (QCNs) representing agents local preferences or beliefs on the relative position of spatial or temporal entities. Two classes of merging operators which, given a set of input QCNs defined on the same qualitative formalism, return a set of qualitative configurations representing a global view of these QCNs, are pointed out. These operators are based on local distances and aggregation functions. In contrast to QCN merging operators recently proposed in the literature, they take account for each constraint from the input QCNs within the merging process. Doing so, inconsistent QCNs do not need to be discarded at start, hence agents reporting locally consistent, yet globally inconsistent pieces of information (due to limited rationality) can be taken into consideration.