nach oben

2015 | Buch

Kapitel lesen Erstes Kapitel lesen

Frontiers of Combining Systems

10th International Symposium, FroCoS 2015, Wroclaw, Poland, September 21-24, 2015, Proceedings

herausgegeben von: Carsten Lutz, Silvio Ranise

Verlag: Springer International Publishing

Buchreihe : Lecture Notes in Computer Science

Enthalten in: Springer Professional "Wirtschaft+Technik" , Springer Professional "Technik" , Springer Professional "Wirtschaft"

Einloggen, um Zugang zu erhalten

Über dieses Buch

This book constitutes the proceedings of the 10th International Symposium on Frontiers of Combining Systems, FroCoS 2015, held in Wroclaw, Poland, in September 2015.

The 20 papers presented in this volume were carefully reviewed and selected from 34 submissions. They were organized in topical sections named: description logics; theorem proving and model building; decision procedures; decision procedures for verification; rewriting and constraint solving; transformations between symbolic systems; combination methods; and reasoning in large theories. The book also contains one invited talk in full-paper length.

Inhaltsverzeichnis

Frontmatter

Invited Talk

Frontmatter

Free Variables and Theories: Revisiting Rigid E-unification

Abstract

The efficient integration of theory reasoning in first-order calculi with free variables (such as sequent calculi or tableaux) is a long-standing challenge. For the case of the theory of equality, an approach that has been extensively studied in the 90s is rigid E-unification, a variant of equational unification in which the assumption is made that every variable denotes exactly one term (rigid semantics). The fact that simultaneous rigid E-unification is undecidable, however, has hampered practical adoption of the method, and today there are few theorem provers that use rigid E-unification.

One solution is to consider incomplete algorithms for computing (simultaneous) rigid E-unifiers, which can still be sufficient to create sound and complete theorem provers for first-order logic with equality; such algorithms include rigid basic superposition proposed by Degtyarev and Voronkov, but also the much older subterm instantiation approach introduced by Kanger in 1963 (later also termed minus-normalisation). We introduce bounded rigid E-unification (BREU) as a new variant of E-unification corresponding to subterm instantiation. In contrast to general rigid E-unification, BREU is NP-complete for individual and simultaneous unification problems, and can be solved efficiently with the help of SAT; BREU can be combined with techniques like congruence closure for ground reasoning, and be used to construct theorem provers that are competitive with state-of-the-art tableau systems. We outline ongoing research how BREU can be generalised to other theories than equality.

Peter Backeman, Philipp Rümmer

Description Logics

Frontmatter

Decidable Description Logics of Context with Rigid Roles

Abstract

To represent and reason about contextualized knowledge often two-dimensional Description Logics (DLs) are employed, where one DL is used to describe contexts (or possible worlds) and the other DL is used to describe the objects, i.e. the relational structure of the specific contexts. Previous approaches for DLs of context that combined pairs of DLs resulted in undecidability in those cases where so-called rigid roles are admitted, i.e. if parts of the relational structure are the same in all contexts. In this paper, we present a novel combination of pairs of DLs and show that reasoning stays decidable even in the presence of rigid roles. We give complexity results for various combinations of DLs including $\mathcal{ALC}$, $\mathcal{SHOQ}$, and $\mathcal{EL}$.

Stephan Böhme, Marcel Lippmann

Adding Threshold Concepts to the Description Logic $\mathcal{EL}$

Abstract

We introduce an extension of the lightweight Description Logic $\mathcal{EL}$ that allows us to define concepts in an approximate way. For this purpose, we use a graded membership function, which for each individual and concept yields a number in the interval [0,1] expressing the degree to which the individual belongs to the concept. Threshold concepts C _~ t for ~ ∈ { < , ≤ , > , ≥ } then collect all the individuals that belong to C with degree ~ t. We generalize a well-known characterization of membership in $\mathcal{EL}$ concepts to construct a specific graded membership function deg, and investigate the complexity of reasoning in the Description Logic $\tau\mathcal{EL}$deg, which extends $\mathcal{EL}$ by threshold concepts defined using deg. We also compare the instance problem for threshold concepts of the form C _> t in $\tau\mathcal{EL}$deg with the relaxed instance queries of Ecke et al.

Franz Baader, Gerhard Brewka, Oliver Fernández Gil

Reasoning in Expressive Description Logics under Infinitely Valued Gödel Semantics

Abstract

Fuzzy Description Logics (FDLs) combine classical Description Logics with the semantics of Fuzzy Logics in order to represent and reason with vague knowledge. Most FDLs using truth values from the interval [0,1] have been shown to be undecidable in the presence of a negation constructor and general concept inclusions. One exception are those FDLs whose semantics is based on the infinitely valued Gödel t-norm (G). We extend previous decidability results for the FDL G-$\mathcal{ALC}$ to deal with complex role inclusions, nominals, inverse roles, and qualified number restrictions. Our novel approach is based on a combination of the known crispification technique for finitely valued FDLs and an automata-based procedure for reasoning in G-$\mathcal{ALC}$.

Stefan Borgwardt, Rafael Peñaloza

Theorem Proving and Model Building

Frontmatter

NRCL - A Model Building Approach to the Bernays-Schönfinkel Fragment

Abstract

We combine constrained literals for model representation with key concepts from first-order superposition and propositional conflict-driven clause learning (CDCL) to create the new calculus Non-Redundant Clause Learning (NRCL) deciding the Bernays-Schönfinkel fragment. We use first-order literals constrained by disequalities between tuples of terms for compact model representation. From superposition, NRCL inherits the abstract redundancy criterion and the monotone model operator. CDCL adds the dynamic, conflict-driven search for a model. As a result, NRCL finds a false clause modulo the current model candidate effectively. It guides the derivation of a first-order ordered resolvent that is never redundant. Similar to 1UIP-learning in CDCL, the learned resolvent induces backtracking and, by blocking the previous conflict state via propagation, it enforces progress towards finding a model or a refutation. The non-redundancy result also implies that only finitely many clauses can be generated by NRCL on the Bernays-Schönfinkel fragment, which proves termination.

Gábor Alagi, Christoph Weidenbach

First-Order Logic Theorem Proving and Model Building via Approximation and Instantiation

Abstract

In this paper we consider first-order logic theorem proving and model building via approximation and instantiation. Given a clause set we propose its approximation into a simplified clause set where satisfiability is decidable. The approximation extends the signature and preserves unsatisfiability: if the simplified clause set is satisfiable in some model, so is the original clause set in the same model interpreted in the original signature. A refutation generated by a decision procedure on the simplified clause set can then either be lifted to a refutation in the original clause set, or it guides a refinement excluding the previously found unliftable refutation. This way the approach is refutationally complete. We do not step-wise lift refutations but lift conflicting cores, finite unsatisfiable clause sets representing at least one refutation. The approach is dual to many existing approaches in the literature.

Andreas Teucke, Christoph Weidenbach

An Expressive Model for Instance Decomposition Based Parallel SAT Solvers

Abstract

SAT solvers are highly efficient programs that decide the satisfiability problem for propositional formulas in conjunctive normal form. Contemporary SAT solvers combine many advanced techniques such as clause sharing and inprocessing. Clause sharing is a form of cooperation in parallel SAT solvers based on clause learning, whereas inprocessing simplifies formulas in a satisfiability-preserving way. In this paper, we present the instance decomposition formalism ID that models parallel SAT solvers with label-based clause sharing and inprocessing. We formally prove soundness of ID and show that the concept of labels can be used to ensure satisfiability-preserving operations. Moreover, we develop a new proof format for SAT solvers based on this approach, which is derived from ID.

Tobias Philipp

Decision Procedures

Frontmatter

Weakly Equivalent Arrays

Abstract

The (extensional) theory of arrays is widely used to model systems. Hence, efficient decision procedures are needed to model check such systems. In this paper, we present an efficient decision procedure for the theory of arrays. We build upon the notion of weak equivalence. Intuitively, two arrays are weakly equivalent if they only differ at finitely many indices. We formalise this notion and show how to exploit weak equivalences to decide formulas in the quantifier-free fragment of the theory of arrays. We present a novel data structure to represent all weak equivalence classes induced by a formula in linear space (in the number of array terms). Experimental evidence shows that this technique is competitive with other approaches.

Jürgen Christ, Jochen Hoenicke

A Decision Procedure for Regular Membership and Length Constraints over Unbounded Strings

Abstract

We prove that the quantifier-free fragment of the theory of character strings with regular language membership constraints and linear integer constraints over string lengths is decidable. We do that by describing a sound, complete and terminating tableaux calculus for that fragment which uses as oracles a decision procedure for linear integer arithmetic and a number of computable functions over regular expressions. A distinguishing feature of this calculus is that it provides a completely algebraic method for solving membership constraints which can be easily integrated into multi-theory SMT solvers. Another is that it can be used to generate symbolic solutions for such constraints, that is, solved forms that provide simple and compact representations of entire sets of complete solutions. The calculus is part of a larger one providing the theoretical foundations of a high performance theory solver for string constraints implemented in the SMT solver CVC4.

Tianyi Liang, Nestan Tsiskaridze, Andrew Reynolds, Cesare Tinelli, Clark Barrett

Adapting Real Quantifier Elimination Methods for Conflict Set Computation

Abstract

The satisfiability problem in real closed fields is decidable. In the context of satisfiability modulo theories, the problem restricted to conjunctive sets of literals, that is, sets of polynomial constraints, is of particular importance. One of the central problems is the computation of good explanations of the unsatisfiability of such sets, i.e. obtaining a small subset of the input constraints whose conjunction is already unsatisfiable. We adapt two commonly used real quantifier elimination methods, cylindrical algebraic decomposition and virtual substitution, to provide such conflict sets and demonstrate the performance of our method in practice.

Maximilian Jaroschek, Pablo Federico Dobal, Pascal Fontaine

Decision Procedures for Verification

Frontmatter

A New Acceleration-Based Combination Framework for Array Properties

Abstract

This paper presents an acceleration-based combination framework for checking the satisfiability of classes of quantified formulae of the theory of arrays. We identify sufficient conditions for which an ‘acceleratability’ result can be used as a black-box module inside such satisfiability procedures. Besides establishing new decidability results and relating them to results from recent literature, we discuss the application of our combination framework to the problem of checking the safety of imperative programs with arrays.

Francesco Alberti, Silvio Ghilardi, Natasha Sharygina

Decidability of Verification of Safety Properties of Spatial Families of Linear Hybrid Automata

Abstract

We consider systems composed of an unbounded number of uniformly designed linear hybrid automata, whose dynamic behavior is determined by their relation to neighboring systems. We present a class of such systems and a class of safety properties whose verification can be reduced to the verification of (small) families of “neighboring” systems of bounded size, and identify situations in which such verification problems are decidable, resp. fixed parameter tractable. We illustrate the approach with an example from coordinated vehicle guidance.

Werner Damm, Matthias Horbach, Viorica Sofronie-Stokkermans

Rewriting and Constraint Solving

Frontmatter

A Completion Method to Decide Reachability in Rewrite Systems

Abstract

The Knuth-Bendix method takes in argument a finite set of equations and rewrite rules and, when it succeeds, returns an algorithm to decide if a term is equivalent to another modulo these equations and rules. In this paper, we design a similar method that takes in argument a finite set of rewrite rules and, when it succeeds, returns an algorithm to decide not equivalence but reachability modulo these rules, that is if a term reduces to another. As an application, we give new proofs of the decidability of reachability in finite ground rewrite systems and in pushdown systems.

Guillaume Burel, Gilles Dowek, Ying Jiang

Axiomatic Constraint Systems for Proof Search Modulo Theories

Abstract

Goal-directed proof search in first-order logic uses meta- variables to delay the choice of witnesses; substitutions for such variables are produced when closing proof-tree branches, using first-order unification or a theory-specific background reasoner. This paper investigates a generalisation of such mechanisms whereby theory-specific constraints are produced instead of substitutions. In order to design modular proof-search procedures over such mechanisms, we provide a sequent calculus with meta-variables, which manipulates such constraints abstractly. Proving soundness and completeness of the calculus leads to an axiomatisation that identifies the conditions under which abstract constraints can be generated and propagated in the same way unifiers usually are. We then extract from our abstract framework a component interface and a specification for concrete implementations of background reasoners.

Damien Rouhling, Mahfuza Farooque, Stéphane Graham-Lengrand, Assia Mahboubi, Jean-Marc Notin

Transformations between Symbolic Systems

Frontmatter

Formalizing Soundness and Completeness of Unravelings

Abstract

Unravelings constitute a class of program transformations to model conditional rewrite systems as standard term rewrite systems. Key properties of unravelings are soundness and completeness with respect to reductions, in the sense that rewrite sequences in the unraveled system correspond to rewrite sequences in the conditional system and vice versa. While the latter is easily satisfied, the former holds only under certain conditions and is notoriously difficult to prove. This paper describes an Isabelle formalization of both properties. The soundness proof is based on the approach by Nishida, Sakai, and Sakabe (2012) but we also contribute to the theory by showing it applicable to a larger class of unravelings.

Based on our formalization we developed the first certifier to check output of conditional rewrite tools. In particular, quasi-decreasingness proofs by AProVE and conditional confluence proofs by ConCon can be certified.

Sarah Winkler, René Thiemann

Proofs and Reconstructions

Abstract

Implementing proof reconstruction is difficult because it involves symbolic manipulations of formal objects whose representation varies between different systems. It requires significant knowledge of the source and target systems. One cannot simply re-target to another logic. We present a modular proof reconstruction system with separate components, specifying their behaviour and describing how they interact. This system is demonstrated and evaluated through an implementation to reconstruct proofs generated by Leo-II and Satallax in Isabelle HOL, and is shown to work better than the current method of rediscovering proofs using a select set of provers.

Nik Sultana, Christoph Benzmüller, Lawrence C. Paulson

Combination Methods

Frontmatter

A Rewriting Approach to the Combination of Data Structures with Bridging Theories

Abstract

We introduce a combination method à la Nelson-Oppen to solve the satisfiability problem modulo a non-disjoint union of theories connected with bridging functions. The combination method is particularly useful to handle verification conditions involving functions defined over inductive data structures. We investigate the problem of determining the data structure theories for which this combination method is sound and complete. Our completeness proof is based on a rewriting approach where the bridging function is defined as a term rewrite system, and the data structure theory is given by a basic congruence relation. Our contribution is to introduce a class of data structure theories that are combinable with a disjoint target theory via an inductively defined bridging function. This class includes the theory of equality, the theory of absolutely free data structures, and all the theories in between. Hence, our non-disjoint combination method applies to many classical data structure theories admitting a rewrite-based satisfiability procedure.

Paula Chocron, Pascal Fontaine, Christophe Ringeissen

Unification and Matching in Hierarchical Combinations of Syntactic Theories

Abstract

We investigate a hierarchical combination approach to the unification problem in non-disjoint unions of equational theories. In this approach, the idea is to extend a base theory with some additional axioms given by rewrite rules in such way that the unification algorithm known for the base theory can be reused without loss of completeness. Additional techniques are required to solve a combined problem by reducing it to a problem in the base theory. In this paper we show that the hierarchical combination approach applies successfully to some classes of syntactic theories, such as shallow theories since the required unification algorithms needed for the combination algorithm can always be obtained. We also consider the matching problem in syntactic extensions of a base theory. Due to the more restricted nature of the matching problem, we obtain several improvements over the unification problem.

Serdar Erbatur, Deepak Kapur, Andrew M. Marshall, Paliath Narendran, Christophe Ringeissen

Combining Forward and Backward Propagation

Abstract

Constraint Handling Rules (CHR) is a general-purpose rule-based programming language. This paper studies the forward and backward propagation of rules, and explores the combination of both execution strategies. Forward propagation transforms input to output, while backward propagation uncovers input from output. This work includes a source-to-source transformation capable of implementing a backward propagation of the rules. Furthermore with the addition of annotating trigger constraints, CHR programs can be executed in a strictly-forward, strictly-backward or combined interleaved quasi-simultaneous manner. A programmer should only write one program and then the annotated transformation empowers the multiple execution strategies. The proposed work is useful for automatic implementation of bidirectional search for any search space through the combined execution strategies. Moreover, it is advantageous for reversible bijective algorithms (such as lossless compression/decompression), requiring only one algorithm direction to be implemented.

Amira Zaki, Slim Abdennadher, Thom Frühwirth

Reasoning in Large Theories

Frontmatter

Random Forests for Premise Selection

Abstract

The success rates of automated theorem provers in large theories highly depend on the choice of given facts. Premise selection is the task of choosing a subset of given facts, which is most likely to lead to a successful automated deduction proof of a given conjecture. Premise selection can be viewed as a multi-label classification problem, where machine learning from related proofs turns out to currently be the most successful method. Random forests are a machine learning technique known to perform especially well on large datasets. In this paper, we evaluate random forest algorithms for premise selection. To deal with the specifics of automated reasoning, we propose a number of extensions to random forests, such as incremental learning, multi-path querying, depth weighting, feature IDF (inverse document frequency), and integration of secondary classifiers in the tree leaves. With these extensions, we improve on the k-nearest neighbour algorithm both in terms of prediction quality and ATP performance.

Michael Färber, Cezary Kaliszyk

Lemmatization for Stronger Reasoning in Large Theories

Abstract

In this work we improve ATP performance in large theories by the reuse of lemmas derived in previous related problems. Given a large set of related problems to solve, we run automated theorem provers on them, extract a large number of lemmas from the proofs found and post-process the lemmas to make them usable in the remaining problems. Then we filter the lemmas by several tools and extract their proof dependencies, and use machine learning on such proof dependencies to add the most promising generated lemmas to the remaining problems. On such enriched problems we run the automated provers again, solving more problems. We describe this method and the techniques we used, and measure the improvement obtained. On the MPTP2078 large-theory benchmark the method yields 6.6% and 6.2% more problems proved in two different evaluation modes.

Cezary Kaliszyk, Josef Urban, Jiří Vyskočil

Backmatter

Titel: Frontiers of Combining Systems
herausgegeben von: Carsten Lutz
Silvio Ranise
Verlag: Springer International Publishing
Electronic ISBN: 978-3-319-24246-0
Print ISBN: 978-3-319-24245-3
DOI: https://doi.org/10.1007/978-3-319-24246-0

Springer Professional

Über dieses Buch

Inhaltsverzeichnis

Frontmatter

Invited Talk

Frontmatter

Free Variables and Theories: Revisiting Rigid E-unification

Description Logics

Frontmatter

Decidable Description Logics of Context with Rigid Roles

Adding Threshold Concepts to the Description Logic $\mathcal{EL}$

Reasoning in Expressive Description Logics under Infinitely Valued Gödel Semantics

Theorem Proving and Model Building

Frontmatter

NRCL - A Model Building Approach to the Bernays-Schönfinkel Fragment

First-Order Logic Theorem Proving and Model Building via Approximation and Instantiation

An Expressive Model for Instance Decomposition Based Parallel SAT Solvers

Decision Procedures

Frontmatter

Weakly Equivalent Arrays

A Decision Procedure for Regular Membership and Length Constraints over Unbounded Strings

Adapting Real Quantifier Elimination Methods for Conflict Set Computation

Decision Procedures for Verification

Frontmatter

A New Acceleration-Based Combination Framework for Array Properties

Decidability of Verification of Safety Properties of Spatial Families of Linear Hybrid Automata

Rewriting and Constraint Solving

Frontmatter

A Completion Method to Decide Reachability in Rewrite Systems

Axiomatic Constraint Systems for Proof Search Modulo Theories

Transformations between Symbolic Systems

Frontmatter

Formalizing Soundness and Completeness of Unravelings

Proofs and Reconstructions

Combination Methods

Frontmatter

A Rewriting Approach to the Combination of Data Structures with Bridging Theories

Unification and Matching in Hierarchical Combinations of Syntactic Theories

Combining Forward and Backward Propagation

Reasoning in Large Theories

Frontmatter

Random Forests for Premise Selection

Lemmatization for Stronger Reasoning in Large Theories

Backmatter

Premium Partner