Polite Theories Revisited

Clausal Graph Tableaux for Hybrid Logic with Eventualities and Difference

Generating Counterexamples for Structural Inductions by Exploiting Nonstandard Models

Symbolic Automata Constraint Solving

Constructors, Sufficient Completeness, and Deadlock Freedom of Rewrite Theories

Infinite families of finite string rewriting systems and their confluence

Extended Computation Tree Logic

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.

Tableau calculus for the logic of comparative similarity over arbitrary distance spaces

The calculus provides a decision procedure for the logic, its termination is obtained by imposing suitable blocking restrictions.

On the Complexity of the Bernays-Sch\"onfinkel Class with Datalog

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.

Clause Elimination Procedures for CNF Formulas

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.

Revisiting Matrix Interpretations for Polynomial Derivational Complexity of Term Rewriting

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.

Boosting local search thanks to CDCL

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.

Improving resource-unaware SAT solvers

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 proﬁling. 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 aﬀecting

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.

A nonmonotonic extension of KLM Preferential Logic P

monotonic extension of Preferential logic P deﬁned by Kraus, Lehmann

and Magidor (KLM). In order to perform nonmonotonic inferences, we

deﬁne 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.

Labelled Unit Superposition Calculi for Instantiation-based Reasoning

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.

Bottom-up Tree Automata with Term Constraints

SAT Encoding of Unification in EL

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.

Characterising Probabilistic Processes Logically

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.

Magically Constraining the Inverse Method with Dynamic Polarity Assignment

Interpolating Quantifier-Free Presburger Arithmetic

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.

Variable Compression in ProbLog

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.

Superposition-Based Analysis of First-Order Probabilistic Timed Automata

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.

Generating Combinatorial Test Cases by Efficient SAT Encodings Suitable for CDCL SAT Solvers

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.

Strong Normalization of the Calculus of Constructions with Type-Based Termination

Focused Natural Deduction

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.

Resolution for Stochastic Boolean Satisfiability

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.

Characterising Space Complexity Classes via Knuth-Bendix Orders

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.

The Consistency of the CADIAG-2 Knowledge Base: A Probabilistic Approach

numerous sets of conflicting rules and compute all of them for its slightly relaxed version.

Lazy Abstraction for Size-Change Termination

Aligators for Arrays

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.

PBINT, a logic for modelling search problems involving arithmetic

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.

On the Complexity of Model Expansion

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.

On the Satisfiability of Two-Variable Logic over Data Words

Generic Methods for Formalising Sequent Calculi Applied to Provability Logic

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.

Using Causal Relationships to Deal with the Ramification Problem in Action Formalisms Based on Description Logics

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.

An Isabelle-like procedural mode for HOL Light

Partitioning SAT Instances for Distributed Solving

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.

Expansion nets: Proof nets for for propositional classical logic

fCube: An Efficient Prover for Intuitionistic Propositional Logic

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.

How to Universally Close the Existential Rule

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.

A Syntactical Approach to Qualitative Constraint Networks Merging