Traditionally, a logic program is built up to reason about atomic first-order formulas. The key idea of parametrized logic programming is that, instead of atomic first-order formulas, a parametrized logic program reasons about formulas of a given parameter logic. We define semantics for such general programs and prove results that can be instantiated for every particular choice of the parameter logic. We show that some known approaches in the literature of logic programming, such as paraconsistent answer-sets and the MKNF semantics for hybrid knowledge bases, are obtained as particular choices of the parameter logic. Joint work with José Alferes.
A reformulation of Parigot's lambda-mu-calculus will be presented, together with applications to proof theory (natural deduction for classical logic, Curry-Howard interpretation of sequent calculus) and to the theory of programming languages (call-by-value lambda-calculus, foundations for let-expressions).
We define and study abstract valuation semantics for logics, an algebraically well-behaved version of valuation semantics. In the context of the behavioral approach to the algebraization of logics (which we briefly overview), we show, by means of meaningful bridge theorems and application examples, that abstract valuations are suited to play a role similar to the one played by logical matrices in the traditional approach to algebraization. Joint work with Ricardo Gonçalves.
What is the minimum number of links in a network whose failure interrupts the flow of traffic from a node X to a node Y? If all paths in the network can be used to carry traffic, then Menger’s theorem provides the answer: the minimum number of links whose failure interrupts the flow of traffic from X to Y equals the maximum number of link-disjoint paths from X to Y, a quantity which can be computed in polynomial-time. However, routing policies preclude some paths from carrying traffic. Moreover, these routing policies are substantiated by routing protocols which, alas, discover some paths all the while hiding others. The bottom line is that, in a networking setting, the question above is not answered by Menger’s theorem or any other result from graph theory. We algebraically identify a broad class of routing policies for which we can answer our opening question with a polynomial-time algorithm. Complementarily, we show the counter-intuitive behavior of routing policies that call out of that class. The theory is applied to a public description of the Internet’s topology to quantify how much of its intrinsic connectivity is lost to current routing policies and how much is recovered with simple alternative ones.
Combined connectives arise in combined logics. In fibrings such combined connectives are known as shared connectives and inherit the logical properties of each component. A new form of combining connectives is proposed by inheriting only the common logical properties of the components. A sound and weakly complete calculus is provided for reasoning about both kinds of combined connectives. Many examples are provided contributing to a better understanding of what are the common properties of any two connectives, say disjunction and conjunction. Joint work with Cristina Sernadas and João Rasga.
Classical negation can be decomposed in various rules of pure negation (rules dealing with negation as the only connective). In this talk we will study the combination of these rules between each other and with pure rules for other connectives. In this setting we will examine in particular the combination of negation with disjunction to understand how the law of excluded middle paradoxically appears, contradicting the standard conservative idea of combination of logics.
Model checking has been extensively used to automatically check properties in large-scale systems. However, the classical techniques only allow for checking of qualitative properties, thus being inadequate for inherently probabilistic systems. Probabilistic model checking (PMC) extends the classical suite of techniques of classical model checking by allowing quantitative reasoning over probabilistic-nondeterministic systems which combine both probabilistic behaviour and nondeterministic choice. Abstraction, the main tool to deal with the “state explosion” problem in the classical setting, is not well developed in the probabilistic setting, limiting the applicability of PMC to little more than checking of reachability properties. Part of the reason for this limited success is that counterexamples in the probabilistic cases are much more complicated objects than their classical counterparts, making counterexample analysis much harder. In this seminar, we will present an abstraction-refinement loop for probabilistic systems based on an extension of the concept of may and must abstractions in the classical setting. May and must abstractions are respectively over and underestimations of the behaviours of a system. For a large class of properties, one of the abstractions preserves satisfaction and the other preserves non-satisfaction, eliminating the need for (expensive) counterexample analysis. Joint work with Anvesh Komuravelli and Edmund Clarke.
Iterative shrinkage/thresholding (IST) algorithms are important elements of the computational toolbox used in signal processing and statistical inference problems, where sparse solutions are sought. Examples, include compressed sensing and signal/image restoration. IST algorithms are typically used to address unconstrained minimization formulations, where the objective function includes a quadratic data term (corresponding to liner observation model under Gaussian noise) and a non-quadratic regularizer (such as an l1 norm or a TV norm). In this talk, after briefly reviewing the several ways in which IST algorithms can be derived, as well as several convergence results, I will present some recent advances: (a) new ways to derive IST-like algorithms, (b) new accelerated versions of IST, (c) new IST-type algorithms tailored to non-Gaussian noise models.
Inspired by the recent notion of importing logics, a new formulation of unconstrained fibring is proposed as a kind of two-way importing (biporting). Biporting and unconstrained fibring are proved to be strongly equivalent at the entailment level, modulo a minor translation of formulas. Importing is recovered from biporting by selecting away the export connective. In consequence, special cases of importing, like temporalization, globalization and other asymmetric mechanisms for combining logics, are shown to be subsumed by fibring under selection. Capitalizing on these results, the finite model property is shown to be preserved by importing and those asymmetric constructions whenever it is preserved by fibring.
When combining logics while imposing the sharing of connectives, the result is frequently inconsistent. In fact, in fibring, fusion and other forms of combination reported in the literature, each shared connective inherits the logical properties of each of its components. A new form of combining logics (meet-combination) is proposed where such a connective inherits only the common logical properties of its components. The conservative nature of the proposed combination is shown to hold without provisos. Preservation of soundness and completeness is also proved. Illustrations are provided involving classical, intuitionistic and modal logics. Joint work with Cristina Sernadas and João Rasga
Product of matrix logics is shown to preserve a slightly relaxed notion of Craig interpolation. The symbolic proof capitalizes on the complete axiomatization of the product of matrix logics provided by meet-combination. The computation of the interpolant in the resulting logic is proved to be polynomially reducible to the computation of the interpolants in the two given logics. Illustrations are provided for classical, intuitionistic and modal propositional logics.
Motivated by questions in semantics of modal (propositional) logics, over the past years several duality results which extend the classical Priestley and Stone dualities were established. These results typically involve some type of Vietoris functor on topological spaces, and, by viewing spaces as (generalised) categories, in this talk we reveal the Vietories functor as part of the covariant presheaf monad. Furthermore, we show how the Kleisli construction for monads allows a common approach for this kind of duality theorems.
Combined connectives arise when combining logics and are also useful for analyzing the common properties of two connectives within a given logic. A non-deterministic semantics and a Hilbert calculus are proposed for the meet-combination of connectives (and other language constructors) of any matrix logic endowed with a Hilbert calculus. The logic enriched with such combined connectives is shown to be a conservative extension of the original logic. It is also proved that both soundness and completeness are preserved. Illustrations are provided for classical propositional logic. Joint work with Cristina Sernadas, Joao Rasga and Paulo Mateus.
The talk will explore a framework in which agents can have two very basic propositional attitudes: asserting and denying. Different sets of postulates characterizing the reasonable behavior of the classic-like agents involved with be seen to give rise to different logics, with either deterministic or nondeterministic broadly truth-functional characterizations. This illustrates an approach that generalizes and overcomes some difficulties confronted by both bivalent semantics and society semantics. In particular, I will show how societies can be built that fully take into account the reasoning of their constituent agents on what concerns the satisfaction of complex sentences beyond a reduced list of ‘initial formulas’. The role and effects of considering different disciplines for information collecting and processing will be emphasized.
In this talk, I will present an extension of the mosaic method to the case of logics arising from the combination of linear tense operators with an "orthogonal" S5-like modality. The technique will be applied to obtain a proof of decidability, a proof of completeness for the corresponding Hilbert-style axiomatization and to develop a mosaic-based tableau system. (From a joint work with Carlos Caleiro and Luca Viganò.)
