Catálogo de publicaciones - libros

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.

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.

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.

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.

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.

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 .

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.

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.

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 ^2. m ) time and O ( n ^2) space algorithm based on transitive closure. Our decision procedure is also equality generating, proof generating, and model generating.

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