Catálogo de publicaciones - libros

In this talk we discuss what, according to my long experience, every computer scientists should know from logic. We concentrate on issues of modelling, interpretability and levels of abstraction.We discuss how the minimal toolbox of logic tools should look like for a computer scientist who is involved in designing and analyzing reliable systems. We shall conclude that many classical topics dear to logicians are less important than usually presented, and that less known ideas from logic may be more useful for the working computer scientist.

The model checking community has proposed numerous definitions of vacuous satisfaction, i.e., formal criteria which tell whether a temporal logic specification holds true on a system model . In this paper we attempt to study the notion of vacuous satisfaction from first principles. We show that despite the apparently vague formulation of the vacuity problem, most proposed notions of vacuity for temporal logic can be cast into a uniform and simple framework, and compare previous approaches to vacuity detection from this unified point of view.

Deductive question answering, the extraction of answers to questions from machine-discovered proofs, is the poor cousin of program synthesis. It involves much of the same technology–theorem proving and answer extraction–but the bar is lower. Instead of constructing a general program to meet a given specification for any input–the program synthesis problem–we need only construct answers for specific inputs; question answering is a special case of program synthesis. Since the input is known, there is less emphasis on case analysis (to construct conditional programs) and mathematical induction (to construct looping constructs), those bugbears of theorem proving that are central to general program synthesis. Program synthesis as a byproduct of automatic theorem proving has been a largely dormant field in recent years, while those seeking to apply theorem proving have been scurrying to find smaller problems, including question answering.

We investigate the possibility of developing a decidable logic which allows expressing a large variety of real world specifications. The idea is to define a decidable subset of many-sorted (typed) first- order logic. The motivation is that types simplify the complexity of mixed quantifiers when they quantify over different types. We noticed that many real world verification problems can be formalized by quantifying over different types in such a way that the relations between types remain simple.

Our main result is a decidable fragment of many-sorted first-order logic that captures many real world specifications.

We give the first single-pass (“on the fly”) tableau decision procedure for computational tree logic (CTL). Our method extends Schwendimann’s single-pass decision procedure for propositional linear temporal logic (PLTL) but the extension is non-trivial because of the interactions between the branching inherent in CTL-models, which is missing in PLTL-models, and the “or” branching inherent in tableau search. Our method extends to many other fix-point logics like propositional dynamic logic (PDL) and the logic of common knowledge (LCK).

The decision problem for CTL is known to be EXPTIME-complete, but our procedure requires 2EXPTIME in the worst case. A similar phenomenon occurs in extremely efficient practical single-pass tableau algorithms for very expressive description logics with EXPTIME-complete decision problems because the 2EXPTIME worst-case behaviour rarely arises. Our method is amenable to the numerous optimisation methods invented for these description logics and has been implemented in the Tableau Work Bench () without these extensive optimisations. Its one-pass nature also makes it amenable to parallel proof-search on multiple processors.

Experiments show that many inequalities involving exponentials and logarithms can be proved automatically by combining a resolution theorem prover with a decision procedure for the theory of real closed fields (RCF). The method should be applicable to any functions for which polynomial upper and lower bounds are known. Most bounds only hold for specific argument ranges, but resolution can automatically perform the necessary case analyses. The system consists of a superposition prover (Metis) combined with John Harrison’s RCF solver and a small amount of code to simplify literals with respect to the RCF theory.

We present a model checking algorithm for HFL1, the first-order fragment of Higher-Order Fixpoint Logic. This logic is capable of expressing many interesting properties which are not regular and, hence, not expressible in the modal -calculus. The algorithm avoids best-case exponential behaviour by localising the computation of functions and can be implemented symbolically using BDDs.

We show how insight into the behaviour of this procedure, when run on a fixed formula, can be used to obtain specialised algorithms for particular problems. This yields, for example, the competitive antichain algorithm for NFA universality but also a new algorithm for a string matching problem.

The monadic fragments of first-order Gödel logics are investigated. It is shown that all finite-valued monadic Gödel logics are decidable; whereas, with the possible exception of one (G), all infinite-valued monadic Gödel logics are undecidable. For the missing case G the decidability of an important sub-case, that is well motivated also from an application oriented point of view, is proven. A tight bound for the cardinality of finite models that have to be checked to guarantee validity is extracted from the proof. Moreover, monadic G, like all other infinite-valued logics, is shown to be undecidable if the projection operator Δ is added, while all finite-valued monadic Gödel logics remain decidable with Δ.

The first-order theory of MALL (multiplicative, additive linear logic) over only equalities is an interesting but weak logic since it cannot capture unbounded (infinite) behavior. Instead of accounting for unbounded behavior via the addition of the exponentials (! and ?), we add least and greatest fixed point operators. The resulting logic, which we call MALL=, satisfies two fundamental proof theoretic properties. In particular, MALL= satisfies cut-elimination, which implies consistency, and has a complete focused proof system. This second result about focused proofs provides a strong normal form for cut-free proof structures that can be used, for example, to help automate proof search. We then consider applying these two results about MALL= to derive a focused proof system for an intuitionistic logic extended with induction and co-induction. The traditional approach to encoding intuitionistic logic into linear logic relies heavily on using the exponentials, which unfortunately weaken the focusing discipline. We get a better focused proof system by observing that certain fixed points satisfy the structural rules of weakening and contraction (without using exponentials). The resulting focused proof system for intuitionistic logic is closely related to the one implemented in Bedwyr, a recent model checker based on logic programming. We discuss how our proof theory might be used to build a computational system that can partially automate induction and co-induction.

We propose and investigate a semantics for (or peer data management systems) where different peers are pairwise related to each other by means of data exchange constraints and trust relationships. These two elements plus the data at the peers’ sites and the local integrity constraints for a peer are made compatible via the proposed semantics by determining a set of , which are the intended virtual instances for the peer. The semantically correct answers from a peer to a query, called its , are defined as those answers that are invariant under all its different solution instances. We show that solution instances can be specified as the models of logic programs with a stable model semantics.