Catálogo de publicaciones - libros

Loops and other unbound control structures constitute a major bottleneck in formal software verification, because correctness proofs over such control structures generally require user interaction: typically, induction hypotheses or invariants must be found or modified by hand. Such interaction involves expert knowledge of the underlying calculus and proof engine. We show that one can replace interactive proof techniques, such as induction, with automated first-order reasoning in order to deal with parallelizable loops. A loop can be parallelized, whenever the execution of a generic iteration of its body depends only on the step parameter and not on other iterations. We use a symbolic dependence analysis that ensures parallelizability. This guarantees soundness of a proof rule that transforms a loop into a universally quantified update of the state change information effected by the loop body. This rule makes it possible to employ automatic first-order reasoning techniques to deal with loops. The method has been implemented in the KeY verification tool. We evaluated its applicability with representative case studies from the domain.

We give necessary and sufficient conditions for the first-order theory of a finitely presented abelian lattice-ordered group to be decidable. We also show that if the number of generators is at most 3, then elementary equivalence implies isomorphism. We deduce from our methods that the theory of the free -algebra on at least 2 generators is undecidable.

If is a consistent theory over a fuzzy predicate logic with Gödel negation (e.g. Gödel logic, product logic) then remains consistent after adding the schema tertium non datur ( ∨ ¬) for sentences (closed formulas). We prove and discuss this.

In this paper we define the concept of a profile, which is a characteristic clause set, corresponding to an -proof in first-order logic, which is invariant under rule permutations. It is shown (via cut-elimination) that the profile is even invariant under a large class of proof transformations (called “simple transformations”), which includes transformations to negation normal form. As proofs having the same profile show the same behavior w.r.t. cut-elimination (which can be formally defined via the method CERES), proofs obtained by simple transformations can be considered as equal in this sense. A comparison with related results based on proof nets is given: in particular it is shown that proofs having the same profile define a larger equivalence class than those having the same proof net.

Connections between games and logic are quite common in the literature: for example, to every analytic proof system with the subformula property (hence admitting cut-elimination) one can associate a game in which a player tries to find a cut-free proof and his opponent can attack parts of the proof constructed since then. Along these lines, formulas correspond to games and proofs correspond to winning strategies. A first connection between many-valued logic and games was discovered by Giles in [9]. A variant of such semantics was used in [4] in order to obtain a uniform proof system with a game-theoretical interpretation for Łukasiewicz, product and Gödel logics. The above mentioned papers are extremely interesting, but we would say that the interest of this game semantics is more proof-theoretical than game-theoretical.

In this paper we investigate the problem of characterizing infinite consequence relation in standard BL-algebras by the adding of new rules. First of all, we note that finitary rules do not help, therefore we need at least one infinitary rule. In fact we show that one infinitary rule is sufficient to obtain strong standard completeness, also in the first-order case. Similar results are obtained for product logic and for Łukasiewicz logic. Finally, we show some applications of our results to probabilistic logic over many-valued events and to first-order many-valued logic. In particular, we show a tight bound to the complexity of BL first-order formulas which are valid in the standard semantics.

A few things are known, and many are unknown, on the automorphism group of the free MV-algebra over  − 1 generators. In this paper we show that this group appears as the stabilizer of in the larger group of all automorphisms of the free cancellative hoop over generators. Both groups have a dual action on the same space, namely the ( − 1)-dimensional cube. The larger group has a richer dynamics, at the expense of loosing the two key features of the McNaughton homeomorphisms: preservation of denominators of rational points, and preservation of the Lebesgue measure. We present here some basic results, some examples, and some problems.

Basic constructions of two different theories are presented. The first one is based on the Łukasiewicz connectives, the second on the max - min connectives. In both cases the joint observable is constructed. As an application the central limit theorem is proved.