Invited Talks

Abstract.There is a well-known correspondence between implicational formulas as types and combinators (or lambda-terms) as inhabitants. The correspondence typically connects with natural deduction systems or axioms. In this talk, I will overview some earlier extensions of the Curry-Howard correspondence to include sequent calculi, including that for a relevance logic (implicational ticket entailment). Then, I will introduce a new sequent calculus for the implicational fragment of intuitionistic logic and show how combinatory inhabitants can be obtained from proofs.

Abstract. Sheaves over topological spaces, introduced by Weyl and developed by Leray, Cartan and Lazard, play a fundamental role in Analysis, Geometry, and Algebra. Prototypical examples are the sheaf of germs of continuous real valued functions on a topological space, or Grothendieck’s sheaf of local rings over the spectrum of the ring. Grothendieck moved from spaces to “sites” in order to generalize the cohomology of modules, following Weil’s tip to prove his conjectures on finite fields. Lawvere observed in the 60’s and it was established in firm ground by Makkai, Reyes and Joyal that the category of sheaves over a site (today a Grothendieck topos) is a mathematical universe of varying objects, governed by an inner logic and a heterodox mathematics. These inner logics lie between classical logic and Brouwer-Heyting intuitionistic logic proposed in the first third of last century as an alternative to Fregean logic and the Cantorian foundations of mathematics. New logical operations arise naturally in this context, particularly in the case of connectives, which go beyond Grotendieck topologies. We will sketch with minimum categorical apparatus the main features of mathematics and logic on sheaves, and concentrate on generic models which establishes a bridge between intutionistic and classical logic, encompassing the uses of forcing in set theory and the basic model theoretic constructions of classic finitary or infinitary logic.

Abstract. Rewriting logic is both a logical framework where many logics can be naturally represented, and a semantic framework where many computational systems and programming languages, including concurrent ones, can be both specified and executed. Maude is a declarative specification and programming language based on rewriting logic. For reasoning about the logics and systems represented in the rewriting logic framework symbolic methods are of great importance. This paper discusses various symbolic methods that address crucial reasoning needs in rewriting logic, how they are supported by Maude and other symbolic engines, and various applications that these methods and engines make possible. Because of the generality of rewriting logic, these methods are widely applicable: they can be used in many areas and can provide useful reasoning components for other reasoning engines.

Abstract. In this work, we explore proof theoretical connections between sequent, nested and labelled calculi. In particular, we show a semantical characterisation of intuitionistic, normal and non-normal modal logics for all these systems, via a case-by-case translation between labelled nested to labelled sequent systems.

Abstract. The exploration of the relationships between Belief Revision and Computational Argumentation has led to significant contributions for both areas; several techniques employed in belief revision are being studied to formalize the dynamics of argumentation frameworks, and the capabilities of the argumentation-based defeasible reasoning are being used to define belief change operators. By briey considering the fundamental ideas of both areas it is possible to examine some of the mutually beneficial cross-application in different proposals that model reasoning mechanisms that combine contributions from the two domains.

Abstract. Although formal system verification has been around for many years, little attention was given to the case where the specification of the system has to be changed. This may occur due to a failure in capturing the client’s requirements or due to some change in the domain (think for example of banking systems that have to adapt to different taxes being imposed). We are interested in having methods not only to verify properties, but also to suggest how the system model should be changed so that a property would be satisfied. For this purpose, we will use techniques from the area of Belief Revision.

Belief revision deals with the problem of changing a knowledge base in view of new information. In the last thirty years, several authors have contributed with change operations and ways of characterising them. However, most of the work concentrates on knowledge bases represented using classical propositional logic. In the last decade, there have been efforts to apply belief revision theory to description and modal logics.

In this talk, I will analyse what is needed for a theory of belief revision which can be applied to the temporal logic CTL. In particular, I will illustrate different alternatives for formalising the concept of revision of CTL specifications. Our interest in this particular logic comes both from practical issues, since it is used for software specification, as from theoretical issues, as it is a non-compact logic and most existing results rely on compactness.

This talk is based mostly on joint work with Aline Andrade and Paulo de Tarso Guerra Oliveira