Skip to main content
main-content

Inhaltsverzeichnis

Frontmatter

The Complexity of Partial-Observation Parity Games

We consider two-player zero-sum games on graphs. On the basis of the information available to the players these games can be classified as follows: (a) partial-observation (both players have partial view of the game); (b) one-sided partial-observation (one player has partial-observation and the other player has complete-observation); and (c) complete-observation (both players have complete view of the game). We survey the complexity results for the problem of deciding the winner in various classes of partial-observation games with

ω

-regular winning conditions specified as parity objectives. We present a reduction from the class of parity objectives that depend on sequence of states of the game to the sub-class of parity objectives that only depend on the sequence of observations. We also establish that partial-observation acyclic games are PSPACE-complete.

Krishnendu Chatterjee, Laurent Doyen

Awareness in Games, Awareness in Logic

Standard game theory models implicitly assume that all significant aspects of a game (payoffs, moves available, etc.) are common knowledge among the players. There are well-known techniques going back to Harsanyi [4] for transforming a game where some aspects are not common knowledge to one where they are common knowledge.

Joseph Y. Halpern

Human and Unhuman Commonsense Reasoning

Ford has introduced a non-monotonic logic, System

LS

, inspired by an empirical study of human non-monotonic reasoning. We define here a defeasible logic

FDL

based on Ford’s logic, and in doing so identify some similarities and differences between Ford’s logic and existing defeasible logics. Several technical results about

FDL

are established, including its inference strength in relation to other defeasible logics.

Michael J. Maher

Gödel Logics – A Survey

The logics we present in this tutorial, Gödel logics, can be characterized in a rough-and-ready way as follows: The language is standard, defined at different levels: propositional, quantified-propositional, first-order. The logics are many-valued, and the sets of truth values considered are (closed) subsets of [0, 1] which contain both 0 and 1. 1 is the ‘designated value,’ i.e., a formula is valid if it receives the value 1 in every interpretation. The truth functions of conjunction and disjunction are minimum and maximum, respectively, and in the first-order case quantifiers are defined by infimum and supremum over subsets of the set of truth values.

Norbert Preining

Tableau Calculus for the Logic of Comparative Similarity over Arbitrary Distance Spaces

The logic

$\mathcal{CSL}$

(first introduced by Sheremet, Tishkovsky, 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

$\mathcal{CSL}$

is defined in terms of models based on different classes of distance spaces and it generalizes the logic S4

u

of topological spaces. In this paper we consider

$\mathcal{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

$\mathcal{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.

Régis Alenda, Nicola Olivetti

Extended Computation Tree Logic

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.

Roland Axelsson, Matthew Hague, Stephan Kreutzer, Martin Lange, Markus Latte

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

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 (DLs) without destroying the decidability of the consistency and the projection problem. We investigate the complexity of these decision problems based on which DL is used as base logic for the action formalism.

Franz Baader, Marcel Lippmann, Hongkai Liu

SAT Encoding of Unification in $\mathcal{EL}$

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

$\mathcal{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

$\mathcal{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

$\mathcal{EL}$

-unification algorithm. On the other hand, this reduction provides us with a proof of the fact that

$\mathcal{EL}$

-unification is in NP that is much simpler than the one given in our previous paper on

$\mathcal{EL}$

-unification.

Franz Baader, Barbara Morawska

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

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.

Mutsunori Banbara, Haruki Matsunaka, Naoyuki Tamura, Katsumi Inoue

Generating Counterexamples for Structural Inductions by Exploiting Nonstandard Models

Induction proofs often fail because the stated theorem is noninductive, 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 noninductive theorems. We explain how to apply a well-known concept from first-order logic, nonstandard models, to the detection of noninductive invariants. Our work was done in the context of the proof assistant Isabelle/HOL and the counterexample generator Nitpick.

Jasmin Christian Blanchette, Koen Claessen

Characterising Space Complexity Classes via Knuth-Bendix Orders

We study three different space complexity classes:

LINSPACE

,

PSPACE

, and

ESPACE

and give complete characterisations for these classes. We employ rewrite systems, whose termination can be shown by Knuth Bendix orders. To capture

LINSPACE

, we consider positively weighted Knuth Bendix orders. To capture

PSPACE

, we consider unary rewrite systems, compatible with a Knuth Bendix order, where we allow for padding of the input. And to capture

ESPACE

, we make use of a non-standard generalisation of the Knuth Bendix order.

Guillaume Bonfante, Georg Moser

Focused Natural Deduction

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

focused natural deduction

. The calculus is shown to be sound and complete with respect to first-order intuitionistic linear natural deduction and the backward linear focusing calculus.

Taus Brock-Nannestad, Carsten Schürmann

How to Universally Close the Existential Rule

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.

Kai Brünnler

On the Complexity of the Bernays-Schönfinkel Class with Datalog

The Bernays-Schönfinkel class with Datalog is a 2-variable fragment of the Bernays-Schönfinkel 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 extend the Bernays-Schönfinkel class with Datalog to a more expressive logic — a fragment of two-variable logic with counting quantifiers extended with the same kind of fixed points. We prove that both satisfiability and entailment for the new logic are decidable in NEXPTIME and we give a matching lower bound for the original logic, which establishes NEXPTIME-completeness of the satisfiability and entailment problems for both of them. Our algorithm is based on a translation to 2-variable logic with counting quantifiers.

Witold Charatonik, Piotr Witkowski

Magically Constraining the Inverse Method Using Dynamic Polarity Assignment

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 the top-down engine for a given mode-correct query by rewriting the program and the query using the Magic Sets Transformation (MST). In previous work, we have shown that focusing can logically characterise the standard notion of bottom-up logic programming if atomic formulas are statically given a certain polarity assignment. In an analogous manner, dynamically assigning polarities can characterise the effect of MST without needing to transform the program or the query. This gives us a new proof of the completeness of MST in purely logical terms, by using the general completeness theorem for focusing. As the dynamic assignment is done in a general logic, the essence of MST can potentially be generalised to larger fragments of logic.

Kaustuv Chaudhuri

Lazy Abstraction for Size-Change Termination

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.

Michael Codish, Carsten Fuhs, Jürgen Giesl, Peter Schneider-Kamp

A Syntactical Approach to Qualitative Constraint Networks Merging

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.

Jean-François Condotta, Souhila Kaci, Pierre Marquis, Nicolas Schwind

On the Satisfiability of Two-Variable Logic over Data Words

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.

Claire David, Leonid Libkin, Tony Tan

Generic Methods for Formalising Sequent Calculi Applied to Provability Logic

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 abstract a large part of the proof in a way which is immediately applicable to other calculi. Our work also provides a machine-checked proof to settle the controversy surrounding the proof of cut-admissibility for

GL

.

Jeremy E. Dawson, Rajeev Goré

Characterising Probabilistic Processes Logically

(Extended 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.

Yuxin Deng, Rob van Glabbeek

fCube: An Efficient Prover for Intuitionistic Propositional Logic

We present

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 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.

Mauro Ferrari, Camillo Fiorentini, Guido Fiorino

Superposition-Based Analysis of First-Order Probabilistic Timed Automata

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. The hierarchic superposition calculus required for the analysis is sound and complete on the first-order formulas generated from FPTAs. It even works well in practice. We illustrate the potential behind it with a real-life DHCP protocol example, which we analyze by means of tool chain support.

Arnaud Fietzke, Holger Hermanns, Christoph Weidenbach

A Nonmonotonic Extension of KLM Preferential Logic P

In this paper, we propose the logic P

min

, which is a nonmonotonic 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 minimal models are those that minimize the number of worlds where ¬□¬

A

holds, that is of

A

-worlds which are not minimal. We also present a tableau calculus for deciding entailment in P

min

.

Laura Giordano, Valentina Gliozzi, Nicola Olivetti, Gian Luca Pozzato

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

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.

Benjamin Grégoire, Jorge Luis Sacchini

Aligators for Arrays (Tool Paper)

This paper presents Aligators, a tool for the generation of universally quantified array invariants. Aligators leverages recurrence solving and algebraic techniques to carry out inductive reasoning over array content. The Aligators’ loop extraction module allows treatment of multi-path loops by exploiting their commutativity and serializability properties. Our experience in applying Aligators on a collection of loops from open source software projects indicates the applicability of recurrence and algebraic solving techniques for reasoning about arrays.

Thomas A. Henzinger, Thibaud Hottelier, Laura Kovács, Andrey Rybalchenko

Clause Elimination Procedures for CNF Formulas

We develop and analyze clause elimination procedures, a specific family of simplification techniques for conjunctive normal form (CNF) formulas. Extending known 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 five new) clause elimination procedures from various perspectives:

size reduction

,

BCP-preservance

,

confluence

, and

logical equivalence

. For the variants not preserving logical equivalence, we show how to reconstruct solutions to original CNFs from satisfying assignments to simplified CNFs. We also identify a clause elimination procedure that does a transitive reduction of the binary implication graph underlying any CNF formula purely on the CNF level.

Marijn Heule, Matti Järvisalo, Armin Biere

Partitioning SAT Instances for Distributed Solving

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 lookahead. The methods are incorporated into the iterative approach and its performance is demonstrated with an extensive comparison against the best sequential solvers in the SAT competition 2009 as well as against two efficient parallel solvers.

Antti E. J. Hyvärinen, Tommi Junttila, Ilkka Niemelä

Infinite Families of Finite String Rewriting Systems and Their Confluence

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 (which decidability is not garanteed).

Jean-Pierre Jouannaud, Benjamin Monate

Polite Theories Revisited

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.

Dejan Jovanović, Clark Barrett

Clausal Graph Tableaux for Hybrid Logic with Eventualities and Difference

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.

Mark Kaminski, Gert Smolka

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

The paper presents the methodology and the results of checking consistency of the knowledge base of CADIAG-2, a large-scale medical expert system. Such knowledge base consists of a large collection of rules representing knowledge about various medical entities (symptoms, signs, diseases...) and relationships between them. The major portion of the rules are uncertain, i.e., they specify

to what degree

a medical entity is

confirmed

by another medical entity or a combination of them. Given the size of the system and the uncertainty it has been challenging to validate its consistency. Recent attempts to partially formalise CADIAG-2’s knowledge base into decidable Gödel logics have shown that, on that formalisation, CADIAG-2 is inconsistent. In this paper we verify this result with an alternative, more expressive formalisation of CADIAG-2 as a set of probabilistic conditional statements and apply a state-of-the-art probabilistic logic solver to determine

satisfiability

of the knowledge base and to extract conflicting sets of rules. As CADIAG-2 is too large to be handled out of the box we describe an approach to split the knowledge base into fragments that can be tested independently and prove that such methodology is complete (i.e., is guaranteed to find all conflicts). With this approach we are able to determine that CADIAG-2 contains numerous sets of conflicting rules and compute all of them for a slightly relaxed version of the knowledge base.

Pavel Klinov, Bijan Parsia, David Picado-Muiño

On the Complexity of Model Expansion

We study the complexity of model expansion (MX), which is the problem of expanding a given finite structure with additional relations to produce a finite model of a given formula. This is the logical task underlying many practical constraint languages and systems for representing and solving search problems, and our work is motivated by the need to provide theoretical foundations for these. We present results on both data and combined complexity of MX for several fragments and extensions of FO that are relevant for this purpose, in particular the guarded fragment GF

k

of FO and extensions of FO and GF

k

with inductive definitions. We present these in the context of the two closely related, but more studied, problems of model checking and finite satisfiability. To obtain results on FO(ID), the extension of FO with inductive definitions, we provide translations between FO(ID) with FO(LFP), which are of independent interest.

Antonina Kolokolova, Yongmei Liu, David Mitchell, Eugenia Ternovska

Labelled Unit Superposition Calculi for Instantiation-Based Reasoning

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 modulo equality employs a superposition-style calculus which generates the instances needed by the ground solver to refine a model of a ground 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, AND/OR trees and OBDDs affect the interplay between the proof procedure and blocking mechanisms for redundancy elimination.

Konstantin Korovin, Christoph Sticksel

Boosting Local Search Thanks to cdcl

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. Considering 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.

Gilles Audemard, Jean-Marie Lagniez, Bertrand Mazure, Lakhdar Saïs

Interpolating Quantifier-Free Presburger Arithmetic

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.

Daniel Kroening, Jérôme Leroux, Philipp Rümmer

Variable Compression in ProbLog

In order to compute the probability of a query, ProbLog represents the proofs of the query as disjunctions of conjunctions, 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.

Theofrastos Mantadelis, Gerda Janssens

Improving Resource-Unaware SAT Solvers

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 industrial SAT Competition 2009 benchmark. For the analysis, the total cycles, 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

MiniSAT2.0

improving its runtime by 20% on average.

Steffen Hölldobler, Norbert Manthey, Ari Saptawijaya

Expansion Nets: Proof-Nets for Propositional Classical Logic

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

expansion/deletion trees

. We then show a subcalculus,

expansion nets

, which in addition to these good properties has a polynomial-time correctness criterion.

Richard McKinley

Revisiting Matrix Interpretations for Polynomial Derivational Complexity of Term Rewriting

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 allows triangular matrix interpretations to infer tighter bounds than the original approach.

Friedrich Neurauter, Harald Zankl, Aart Middeldorp

An Isabelle-Like Procedural Mode for HOL Light

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.

Petros Papapanagiotou, Jacques Fleuriot

Bottom-Up Tree Automata with Term Constraints

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.

Andreas Reuß, Helmut Seidl

Constructors, Sufficient Completeness, and Deadlock Freedom of Rewrite Theories

Sufficient completeness has been throughly studied for equational specifications, where function symbols are classified into

constructors

and

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

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

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, deadlock freedom, and other related properties, by propositional 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 an example.

Camilo Rocha, José Meseguer

PBINT, A Logic for Modelling Search Problems Involving Arithmetic

Motivated by computer science challenges, Grädel and Gurevich [13] 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 [27], we use a framework based on embedded model theory, but with a different background structure, the structure of arithmetic which contains at least (ℕ; 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 [27] (and thus indirectly [13]) 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.

Shahab Tasharrofi, Eugenia Ternovska

Resolution for Stochastic Boolean Satisfiability

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.

Tino Teige, Martin Fränzle

Symbolic Automata Constraint Solving

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.

Margus Veanes, Nikolaj Bjørner, Leonardo de Moura

Backmatter

Weitere Informationen

Premium Partner

    Bildnachweise