The algebraic method for theorem proving based on the reduction of first-order formulas within certain rings (commutative rings with unity) equipped with infinitary operations is shown to indicate a possible candidate for a new version of algebrization of FOL, at the same time where the notion of logical derivability is characterized by the notion of algebraic solubility. The topics I intend to discuss are the following:

1. the polynomial ring method as an alternative to algebraizing logic;
2. the notion of $M$-ring, that allows us to operate with some kind of infinitary version of Boolean sums and products;
3. FOL in polynomial version;
4. soundness and completeness of the polynomial ring method for FOL.

Work in progress, joint with M. Matulovic and H. L. Mariano.

I will discuss the first step towards constructing a paraconsistent theory of probability based on the Logics of Formal Inconsistency (LFIs).  It will be shown that LFIS very naturally encode an extension of the notion of probability able to express sophisticate probabilistic reasoning under contradictions. This is achieved by means of appropriate notions of conditional probability and paraconsistent updating, via a version of Bayes' Theorem for conditionalization. It will be also shown that the dissimilarity between the notions of inconsistency and contradiction, one of the pillars of LFIs, plays a central role in this proposed extension of the notion of probability.

Work in progress. Joint work with W. A. Carnielli.

In this talk I will present a component algebra and an associated logic for heterogenous timed systems. The components of the algebra are asynchronous networks of processes that abstract the behaviour of machines that execute according to the clock granularity of the network node in which they are placed and communicate asynchronously with machines at other nodes. The main novelty of this theory is that not all network nodes need to have the same clock granularity. I will discuss conditions under which it can be guaranteed, a priori, that any interconnections generated at run time through dynamic binding of machines with different clock granularities leads to a consistent orchestration of the whole system. I will provide an automata-theoretic view of these results and discuss which logics can support specifications for this component algebra.

This is joint work with J. L. Fiadeiro,  B. Delahaye and A. Legay.

In this talk we introduce $\mathbf{HHL}$, a hierarchical variant of hybrid logic. In particular, we study first order correspondence results and we present a Hennessy-Milner like theorem relating (hierarchical) bisimulation and modal equivalence for $\mathbf{HHL}$. We also discuss decidability and completeness of this logic.

In this talk I will recall how the project of universal logic has emerged and developed: by analogy to univeral algabra, inspired by Tarski's consequence operator and Bourbaki's structural approach. I will outline the future of this project, the idea being not only to develop tools and frameworks for a general theory of logical systems but also to promote logic in all its aspects: philosophical, computational, mathematical, linguistical, a general perspective for rationality and scientific research.

Admissible rules are shown to be preserved by the product of matrix logics. A basis is given for the product, providing that the components enjoy some mild conditions, taking into account reflection results of admissible rules. Structural completeness and decidability of admissible rules are shown to be preserved.  Finally the complexity of the decision algorithm is also analyzed. The results capitalize on the complete axiomatization of the product of matrix logics provided by their meet-combination.

The talk reports on ongoing joint work with Cristina Sernadas and Amílcar Sernadas.

Girard-Reynolds polymorphic lambda calculus [Girard71,Reynolds74], also known as system $\mathbf{F}$, is an elegant system introduced in the early seventies with only two generators of types (formulas): implication and second-order universal quantification. Its impredicative feature - second-order quantifications may instantiate arbitrary types - explains the remarkable expressive power of $\mathbf{F}$ but also the difficulty of reasoning about the system. In the present talk we are interested in a predicative variant of system $\mathbf{F}$, known as the atomic polymorphic calculus [Ferreira06], or system $\mathbf{F}_{\mathbf{at}}$. $\mathbf{F}_{\mathbf{at}}$ has the exact same types (formulas) as $\mathbf{F}$, but a severe restriction on the range of the type variables: only atomic universal instantiations are allowed. We present $\mathbf{F}_{\mathbf{at}}$ and give an overview of some proof-theoretic properties of the system such as the strong normalization property [FerreiraFerreira12], the subformula property [Ferreira06], the sound and faithful embedding of the full intuitionistic propositional calculus into $\mathbf{F}_{\mathbf{at}}$ [FerreiraFerreira09, FerreiraFerreira2015], the disjunction property [Ferreira06], etc. Moreover, we claim that $\mathbf{F}_{\mathbf{at}}$ is the proper setting for the intuitionistic propositional calculus, avoiding this way the connectives $\bot$ and $\vee$, whose natural deduction elimination rules have been subject to harsh criticism (see [Girard(1989B)] pages 74, 80), and avoiding the ad hoc commuting conversion needed in the usual presentation of the latter calculus.

We propose and study a logic able to state and reason about equational constraints, by combining aspects of classical propositional logic, equational logic, and quantifiers. The logic has a classical structure over an algebraic base, and a form of universal quantification distinguishing between local and global validity of equational constraints. We present a sound and complete axiomatization for the logic, parameterized by an equational specification of the algebraic base. We also show (by reduction to SAT) that the logic is decidable, under the assumption that its algebraic base is given by a convergent rewriting system, thus covering an interesting range of examples. As an application, we analyze offline guessing attacks to security protocols, where the equational base specifies the algebraic properties of the cryptographic primitives.

This is joint work with Carlos Caleiro.

I will start by presenting the basic notions of Set Theory such as ordinal and cardinal numbers and afterwards I will review some classical applications of Set Theory to Topological Groups, Banach Algebras and Homological Algebra. I will try to give an intuition of why Set Theory applies to those situations. Following this, I will present some more recent applications of Set Theory to C*-algebras and speculate on how ultimately a connection to mathematical physics may result.

Probabilistic entailment over the classical propositional language is shown to collapse into the classical propositional entailment. Motivated by this result, a probabilistic propositional logic over propositional language endowed with probabilistic assertions is proposed. A sound and weakly complete axiomatization is provided by capitalizing on the decidability of the theory of ordered real-closed fields. This logic is proved to be a conservative extension of classical propositional logic. The talk reports on joint work with Amílcar Sernadas and Cristina Sernadas.