Logics, Theories, and Decision Procedures I

A Comprehensive Framework for Combined Decision Procedures

Abstract

We define a general notion of a fragment within higher order type theory; a procedure for constraint satisfiability in combined fragments is outlined, following Nelson-Oppen schema. The procedure is in general only sound, but it becomes terminating and complete when the shared fragment enjoys suitable noetherianity conditions and allows an abstract version of a ‘Keisler-Shelah like’ isomorphism theorem. We show that this general decidability transfer result covers as special cases, besides applications which seem to be new, the recent extension of Nelson-Oppen procedure to non-disjoint signatures [16] and the fusion transfer of decidability of consistency of A-Boxes with respect to T-Boxes axioms in local abstract description systems [9]; in addition, it reduces decidability of modal and temporal monodic fragments [32] to their extensional and one-variable components.

Silvio Ghilardi, Enrica Nicolini, Daniele Zucchelli

Connecting Many-Sorted Structures and Theories Through Adjoint Functions

Abstract

In a previous paper, we have introduced a general approach for connecting two many-sorted theories through connection functions that behave like homomorphisms on the shared signature, and have shown that, under appropriate algebraic conditions, decidability of the validity of universal formulae in the component theories transfers to their connection. This work generalizes decidability transfer results for so-called ε-connections of modal logics. However, in this general algebraic setting, only the most basic type of ε-connections could be handled. In the present paper, we overcome this restriction by looking at pairs of connection functions that are adjoint pairs for partial orders defined in the component theories.

Franz Baader, Silvio Ghilardi

Combining Data Structures with Nonstably Infinite Theories Using Many-Sorted Logic

Abstract

Most computer programs store elements of a given nature into container-based data structures such as lists, arrays, sets, and multisets. To verify the correctness of these programs, one needs to combine a theory S modeling the data structure with a theory T modeling the elements. This combination can be achieved using the classic Nelson-Oppen method only if both S and T are stably infinite.

The goal of this paper is to relax the stable infiniteness requirement. To achieve this goal, we introduce the notion of polite theories, and we show that natural examples of polite theories include those modeling data structures such as lists, arrays, sets, and multisets. Furthemore, we provide a method that is able to combine a polite theory S with any theory T of the elements, regardless of whether T is stably infinite or not.

The results of this paper generalize to many-sorted logic those recently obtained by Tinelli and Zarba concerning the combination of shiny theories with nonstably infinite theories in one-sorted logic.

Silvio Ranise, Christophe Ringeissen, Calogero G. Zarba

On a Rewriting Approach to Satisfiability Procedures: Extension, Combination of Theories and an Experimental Appraisal

Abstract

The rewriting approach to \(\mathcal{T}\)-satisfiability is based on establishing termination of a rewrite-based inference system for first-order logic on the \(\mathcal{T}\)-satisfiability problem. Extending previous such results, including the quantifier-free theory of equality and the theory of arrays with or without extensionality, we prove termination for the theories of records with or without extensionality, integer offsets and integer offsets modulo. A general theorem for termination on combinations of theories, that covers any combination of the theories above, is given next. For empirical evaluation, the rewrite-based theorem prover E is compared with the validity checkers CVC and CVC Lite, on both synthetic and real-world benchmarks, including both valid and invalid instances. Parametric synthetic benchmarks test scalability, while real-world benchmarks test ability to handle huge sets of literals. Contrary to the folklore that a general-purpose prover cannot compete with specialized reasoners, the experiments are overall favorable to the theorem prover, showing that the rewriting approach is both elegant and practical.

Alessandro Armando, Maria Paola Bonacina, Silvio Ranise, Stephan Schulz

Interface Formalisms

Sociable Interfaces

Abstract

Interface formalisms are able to model both the input requirements and the output behavior of system components; they support both bottom-up component-based design, and top-down design refinement. In this paper, we propose “sociable” interface formalisms, endowed with a rich compositional semantics that facilitates their use in design and modeling. Specifically, we introduce interface models that can communicate via both actions and shared variables, and where communication and synchronization covers the full spectrum, from one-to-one, to one-to-many, many-to-one, and many-to-many. Thanks to the expressive power of interface formalisms, this rich compositional semantics can be realized in an economical way, on the basis of a few basic principles. We show how the algorithms for composing, checking the compatibility, and refining the resulting sociable interfaces can be implemented symbolically, leading to efficient implementations.

Luca de Alfaro, Leandro Dias da Silva, Marco Faella, Axel Legay, Pritam Roy, Maria Sorea

Logics, Theories, and Decision Procedures II

About the Combination of Trees and Rational Numbers in a Complete First-Order Theory

Abstract

Two infinite structures (sets together with operations and relations) hold our attention here: the trees together with operations of construction and the rational numbers together with the operations of addition and substraction and a linear dense order relation without endpoints. The object of this paper is the study of the evaluated trees, a structure mixing the two preceding ones.

First of all, we establish a general theorem which gives a sufficient condition for the completeness of a first-order theory. This theorem uses a special quantifier, primarily asserting the existence of an infinity of individuals having a given first order property. The proof of the theorem is nothing other than the broad outline of a general algorithm which decides if a proposition or its negation is true in certain theories.

We introduce then the theory T _E of the evaluated trees and show its completeness using our theorem. From our proof it is possible to extract a general algorithm for solving quantified constraints in T _E .

Khalil Djelloul

A Complete Temporal and Spatial Logic for Distributed Systems

Abstract

In this paper, we introduce a spatial and temporal logic for reasoning about distributed computation. The logic is a combination of an extension of hybrid logic, that allows us to reason about the spatial structure of a computation, and linear temporal logic, which accounts for the temporal aspects. On the pragmatic side, we show the wide applicability of this logic by means of many examples. Our main technical contribution is completeness of the logic both with respect to spatial/temporal structures and a class of spatial transition systems.

Dirk Pattinson, Bernhard Reus

Constraint Solving and Programming

Hybrid CSP Solving

Abstract

In this paper, we are concerned with the design of a hybrid resolution framework. We develop a theoretical model based on chaotic iterations in which hybrid resolution can be achieved as the computation of a fixpoint of elementary functions. These functions correspond to basic resolution techniques and their applications can easily be parameterized by different search strategies. This framework is used for the hybridization of local search and constraint propagation, and for the integration of genetic algorithms and constraint propagation. Our prototype implementation gave experimental results showing the interest of the model to design such hybridizations.

Eric Monfroy, Frédéric Saubion, Tony Lambert

An Efficient Decision Procedure for UTVPI Constraints

Abstract

A unit two variable per inequality (UTVPI) constraint is of the form a.x+b.y ≤ d where x and y are integer variables, the coefficients a,b ∈ {–1,0,1} and the bound d is an integer constant. This paper presents an efficient decision procedure for UTVPI constraints. Given m such constraints over n variables, the procedure checks the satisfiability of the constraints in O(n.m) time and O(n+m) space. This improves upon the previously known O(n ².m) time and O(n ²) space algorithm based on transitive closure. Our decision procedure is also equality generating, proof generating, and model generating.

Shuvendu K. Lahiri, Madanlal Musuvathi

Declarative Constraint Programming with Definitional Trees

Abstract

The new generic scheme CFLP(\(\mathcal{D}\)) has been recently proposed in [14] as a logical and semantic framework for lazy Constraint Functional Logic Programming over a parametrically given constraint domain \(\mathcal{D}\). Further, [15] presented a Constrained Lazy Narrowing Calculus \(CLNC(\mathcal{D})\) as a convenient computation mechanism for solving goals for CFLP(\(\mathcal{D}\))-programs, which was proved sound and strongly complete with respect to CFLP(\(\mathcal{D}\))’s semantics. Now, in order to provide a formal foundation for an efficient implementation of goal solving methods in existing systems such as Curry [8] and \(\mathcal{TOY}\) [13,6], this paper enriches the CFLP(\(\mathcal{D}\)) framework by presenting an optimization of the CLNC(\(\mathcal{D}\)) calculus by means of definitional trees to efficiently control the computation. We prove that this new Constrained Demanded Narrowing Calculus CDNC(\(\mathcal({D}\)) preserves the soundness and completeness properties of CLNC(\(\mathcal{D}\)) and maintains the good properties shown for needed and demand-driven narrowing strategies [4,11,17].

Rafael del Vado Vírseda

Logical Problem Analysis and Encoding I

Logical Analysis of Hash Functions

Abstract

In this paper we report on a novel approach for uniform encoding of hash functions (but also other cryptographic functions) into propositional logic formulae, and reducing cryptanalysis problems to the satisfiability problem. The approach is general, elegant, and does not require any human expertise on the construction of a specific cryptographic function. By using this approach, we developed a technique for generating hard and satisfiable propositional formulae and hard and unsatisfiable propositional formulae. In addition, one can finely tune the hardness of generated formulae. This can be very important for different applications, including testing (complete or incomplete) sat solvers. The uniform logical analysis of cryptographic functions can be used for comparison between different functions and can expose weaknesses of some of them (as shown for md4 in comparison with md5).

Dejan Jovanović, Predrag Janičić

Combination Issues in Rewriting and Programming

Proving and Disproving Termination of Higher-Order Functions

Abstract

The dependency pair technique is a powerful modular method for automated termination proofs of term rewrite systems (TRSs). We present two important extensions of this technique: First, we show how to prove termination of higher-order functions using dependency pairs. To this end, the dependency pair technique is extended to handle (untyped) applicative TRSs. Second, we introduce a method to prove non-termination with dependency pairs, while up to now dependency pairs were only used to verify termination. Our results lead to a framework for combining termination and non-termination techniques for first- and higher-order functions in a very flexible way. We implemented and evaluated our results in the automated termination prover AProVE.

Jürgen Giesl, René Thiemann, Peter Schneider-Kamp

Proving Liveness with Fairness Using Rewriting

Abstract

In this paper we combine rewriting techniques with verification issues. More precisely, we show how techniques for proving relative termination of term rewrite systems (TRSs) can be applied to prove liveness properties in fair computations. We do this using a new transformation which is stronger than the sound transformation from [5] but still is suitable for automation. On the one hand we show completeness of this approach under some mild conditions. On the other hand we show how this approach applies to some examples completely automatically, using the TPA tool designed for proving relative termination of TRSs. In particular we succeed in proving liveness in the classical readers-writers synchronization problem.

Adam Koprowski, Hans Zantema

A Concurrent Lambda Calculus with Futures

Abstract

We introduce a new concurrent lambda calculus with futures, λ (fut), to model the operational semantics of Alice, a concurrent extension of ML. λ (fut) is a minimalist extension of the call-by-value λ-calculus that yields the full expressiveness to define, combine, and implement a variety of standard concurrency constructs such as channels, semaphores, and ports. We present a linear type system for λ (fut) by which the safety of such definitions and their combinations can be proved: Well-typed implementations cannot be corrupted in any well-typed context.

Joachim Niehren, Jan Schwinghammer, Gert Smolka

Compositional System Design and Refinement

The ASM Method for System Design and Analysis. A Tutorial Introduction

Abstract

We introduce into and survey the ASM method for high-level system design and analysis. We explain the three notions—Abstract State Machine [37], ASM ground model (system blueprint) [7] and ASM refinement [8]—that characterize the method, which integrates also current validation and verification techniques. We illustrate how the method allows the system engineer to rigorously capture requirements by ASM ground models and to stepwise refine these to code in a validatable and verifiable way.

Egon Börger

Logical Problem Analysis and Encoding II

Matching Classifications via a Bidirectional Integration of SAT and Linguistic Resources

Abstract

Classifications, often mistakenly called directories, are pervasive: we use them to classify our messages, our favourite Web Pages, our files, ... And many more can be found in the Web; think for instance of the Google and Yahoo’s directories. The problem is that all these classifications are very different or more precisely, semantically heterogeneous. The most striking consequence is that they classify documents very differently, making therefore very hard and sometimes impossible to find them.

Matching classifications is the process which allows us to map those nodes of two classifications which, intuitively, correspond semantically to each other. In the first part of the talk I will show how it is possible to encode this problem into a propositional validity problem, thus allowing for the use of SAT reasoners. This is done mainly using linguistic resources (e.g., WordNet) and some amount of Natural Language Processing. However, as shown in the second part of the talk, this turns out to be almost useless. In most cases, in fact, linguistic resources do not contain enough of the axioms needed to prove unsatisfiability. The solution to this problem turns to be that of using SAT as a way to generate the missing axioms.

We have started using linguistic resources to provide SAT with the axioms needed to match classifications, and we have ended up using SAT to generate missing axioms in the linguistic resources. We will argue that this is an example of a more general phenomenon which arises when using commonsense knowledge. This in turns becomes an opportunity for the use of decision procedures for a focused automated generation of the missing knowledge.

Fausto Giunchiglia

Theorem Proving Frameworks and Systems

Connecting a Logical Framework to a First-Order Logic Prover

Abstract

We present one way of combining a logical framework and first-order logic. The logical framework is used as an interface to a first-order theorem prover. Its main purpose is to keep track of the structure of the proof and to deal with the high level steps, for instance, induction. The steps that involve purely propositional or simple first-order reasoning are left to a first-order resolution prover (the system Gandalf in our prototype). The correctness of this interaction is based on a general meta-theoretic result. One feature is the simplicity of our translation between the logical framework and first-order logic, which uses implicit typing. Implementation and case studies are described.

Andreas Abel, Thierry Coquand, Ulf Norell

Combination of Isabelle/HOL with Automatic Tools

Abstract

We describe results and status of a sub project of the Verisoft [1] project. While the Verisoft project aims at verification of a complete computer system starting with hardware and up to user applications, the goal of our sub project is an efficient hardware verification.

We use the Isabelle theorem prover [2] as the major tool for hardware design and verification. Since many hardware verification problems can be efficiently solved by automatic tools, we combine Isabelle with model checkers and SAT solvers. This combination of tools speeds up verification of hardware and simplifies sharing of the results with verification of the whole computer system. To increase the range of problems which can be solved by external tools we implemented in Isabelle several algorithms for handling uninterpreted functions and data abstraction.

The resulting combination was applied to verify many different hardware circuits, automata, and processors.

In our project we use open source tools that are free for academical and commercial purposes.

Sergey Tverdyshev

ATS: A Language That Combines Programming with Theorem Proving

Abstract

ATS is a language with a highly expressive type system that supports a restricted form of dependent types in which programs are not allowed to appear in type expressions. The language is separated into two components: a proof language in which (inductive) proofs can be encoded as (total recursive) functions that are erased before execution, and a programming language for constructing programs to be evaluated. This separation enables a paradigm that combines programming with theorem proving. In this paper, we illustrate by example how this programming paradigm is supported in ATS.

Sa Cui, Kevin Donnelly, Hongwei Xi

Springer Professional

Frontiers of Combining Systems

5th International Workshop, FroCoS 2005, Vienna, Austria, September 19-21, 2005. Proceedings

Inhaltsverzeichnis

Frontmatter

Logics, Theories, and Decision Procedures I

A Comprehensive Framework for Combined Decision Procedures

Connecting Many-Sorted Structures and Theories Through Adjoint Functions

Combining Data Structures with Nonstably Infinite Theories Using Many-Sorted Logic

On a Rewriting Approach to Satisfiability Procedures: Extension, Combination of Theories and an Experimental Appraisal

Interface Formalisms

Sociable Interfaces

Logics, Theories, and Decision Procedures II

About the Combination of Trees and Rational Numbers in a Complete First-Order Theory

A Complete Temporal and Spatial Logic for Distributed Systems

Constraint Solving and Programming

Hybrid CSP Solving

An Efficient Decision Procedure for UTVPI Constraints

Declarative Constraint Programming with Definitional Trees

Logical Problem Analysis and Encoding I

Logical Analysis of Hash Functions

Combination Issues in Rewriting and Programming

Proving and Disproving Termination of Higher-Order Functions

Proving Liveness with Fairness Using Rewriting

A Concurrent Lambda Calculus with Futures

Compositional System Design and Refinement

The ASM Method for System Design and Analysis. A Tutorial Introduction

Logical Problem Analysis and Encoding II

Matching Classifications via a Bidirectional Integration of SAT and Linguistic Resources

Theorem Proving Frameworks and Systems

Connecting a Logical Framework to a First-Order Logic Prover

Combination of Isabelle/HOL with Automatic Tools

ATS: A Language That Combines Programming with Theorem Proving

Backmatter

Premium Partner