The study of combined logics is certainly a key issue of the general theory of universal logic. Fibring is a very powerful and appealing mechanism for combining logics. As proposed by Dov Gabbay, fibring should combine L1 and L2 into a system which is the smallest logical system for the combined language which is a conservative extension of both L1 and L2. Of course, a conservative extension of two given logics does not always exist, but in that case one should aim for being as conservative as possible. We know that, given consequence relations for L1 and L2, one just wants the smallest consequence relation over the combined language that extends the two. This corresponds precisely to putting together the axiomatizations of the two logics. However, even if some particular cases have been thoroughly studied and understood, e.g. fusion of modal logics, a general study of this syntactical construction is still lacking. In this paper, we study general conditions for conservativity of fibred logics. To guarantee conservativity, it is certainly necessary that the two consequence systems are coincident when restricted to the common language. We show that this does not suffice and present extra conditions that do. In the particular case of unconstrained fibring - when the signatures are disjoint - we completely characterise the cases where it is conservative. Moreover, as a subproduct, we obtain that unconstrained fibring preserves decidability. These results generalize what was known in the case of fusion of modal logics, covering also some well known open cases, like the fibring of classical and intuitionistic propositional logics.

As we know there are 16 binary connectives that can be defined using bivalent truth-tables. These are - all together or subsets of them - considered to define classical propositional logic. Positive classical propositional logic is just one subsystem using the truth-tables of conjunction. disjunction and implication. If we consider the power set of these 16 connectives, we may wonder how many different subsystems of classical logic we have? (It is easy to define equivalence between such systems using definability) We will investigate in particular the maximal ones relatively to classical logic, which can served as the basis of interesting non-truth-functional bivalent paraconsistent systems stronger than CluN, C1, etc.

We define the notion of a catalytic-space computation. This is a computation that has a small amount of clean space available and is equipped with additional auxiliary space, with the caveat that the additional space is initially in an arbitrary, possibly incompressible, state and must be returned to this state when the computation is finished. We show that the extra space can be used in a nontrivial way, to compute uniform TC1-circuits with just a logarithmic amount of clean space. The extra space thus works analogously to a catalyst in a chemical reaction. (TC1-circuits can compute for example the determinant of a matrix, which is not known to be computable in logspace.) In order to obtain our results we study an algebraic model of computation, a variant of straight-line programs. We employ register machines with input registers \(x_1 , \dots, x_n\) and work registers \(r_1 ,\dots , r_m\). The instructions available are of the form \(r_i \leftarrow r_i \pm u \times v\), with \(r_i\) a register and, \(u, v\) distinct registers or constants. We wish to compute a function \(f (x_1 ,\dots , x_n )\) through a sequence of such instructions. The working registers have some arbitrary initial value \(r_i = \tau_i\), and they may be altered throughout the computation, but by the end all registers must be returned to their initial value \(\tau_i\), except for, say, \(r_1\) which must hold \(\tau_1 + f (x_1 , \dots , x_n )\). We show that all of Valiant’s class VP, and more, can be computed in this model. This significantly extends the framework and techniques of Ben-Or and Cleve [1].

This is joint work with Harry Buhrman, Richard Cleve, Michal Koucký and Florian Speelman.

1. M. Ben-Or and R. Cleve. Computing algebraic formulas using a constant number of registers. SIAM Journal on Computing, 21(1):54–58, 1992.

A central topic in the theory of dynamical systems is to understand the asymptotic behavior that dynamical systems can typically present. In many cases trajectories will converge to some kind of attractor, which can be a fixed point, a periodic orbit, or other type of object like a strange attractor. In this talk we will study the computability of attractors, including fixed points, periodic orbits, and some (partially) hyperbolic attractors like the Smale horseshoe or the geometrical Lorenz attractor.

Many-valued logics received several criticism since its birth. Among the main opponents to its creation there is the Polish logician Roman Suszko. In the mid 70s, at a conferece held in Cracow, he called into question the nature of many-valuedness by claiming the existence of “only but two truth values”, a statement nowadays regarded as Suszko's Thesis, and stated that “after 50 years we still face an illogical paradise of many truths and falsehoods”. Suszko's motivation for his ideas lies in defending the existence of a double semantic role expressed by truth values. This duplicity is revealed by him in drawing the difference between algebraic and logical values. According to him, even though we can have more than two algebraic values, there are only two genuine logical ones. The philosophical content of his ideas finds support in a well know result called Suszko's reduction, a theorem that affirms every tarskian logic is two-valued. Several contributions emerged from Suszko's ideas. It is the purpose of the present talk to expose some of these main developments. At first, it will be shown some results that corroborates Suszko's ideas and present some limitations to them. Lastly, some discussions and comments regarding Suszko's thesis will be shown.

In 1979 Richard Statman proved, using proof-theory, that the purely implicational fragment of Intuitionistic Logic is PSPACE-complete. He showed a polynomially bounded translation from full Intuitionistic Propositional Logic into its implicational fragment. By the PSPACE-completeness of S4, proved by Ladner, and the Godel translation from S4 into Intuitionistic Logic, the PSPACE-completeness of purely implicational fragment of Intuitionistic Logic is drawn. The sub-formula principle for a deductive system for a logic $L$ states that whenever $\{\gamma_1,\ldots,\gamma_k\} \vdash_{L} \alpha$ there is a proof in which each formula occurrence is either a sub-formula of $\alpha$ or of some of $\gamma_i$. In this work we extend Statman's result and show that any propositional (possibly modal) structural logic satisfying a particular statement of the sub-formula principle is PSPACE-complete. As a consequence, EXPTIME-complete propositional logics, such as PDL and the common-knowledge epistemic logic with at least 2 agents satisfy this particular sub-formula principle, if and only if, PSPACE=EXPTIME.

This talk will discuss how computational models defined in toposes may lead to non-standard computational models. A possible comparison with hyper-computation is lightly motivated.

There exist infinitely many ways to extend the classical propositional connectives to the set $[0,1]$, preserving their behaviors in the extremes $0$ and $1$ exactly as in the classical logic. However, it is a consensus that this issue is not sufficient, and, therefore, these extensions must also preserve some minimal logical properties of the classical connectives. The notions of $t$-norms (conjunction), $t$-conorms (disjunction), fuzzy negations and fuzzy implications taking these considerations into account. In previous works, the author, joint with other colleagues, generalizes these notions to the set $\mathbb{U}=\{[a,b]\;|\; 0\leq a\leq b\leq 1\}$ , providing canonical constructions to obtain, for example, interval-valued $t$-norms that are the best interval representations of $t$-norms. In this talk, we will make a revision of fuzzy negations,  interval-valued fuzzy negations and provide  generalizations, in a natural way, of several notions related with fuzzy negations, such as the ones of equilibrium point and negation-preserving automorphism. We show that the main properties of these notions are preserved in those generalizations.

During the 50's, Moore and Sunaga proposed an arithmetic for closed intervals, $[a,b]=\{x\in R: a\leq x\leq b\}$, in order to provide an object able to capture the numerical errors during computations. The idea is that if we want to compute a value, $f(x)$, for  a function $f:\mathbb{R}\to \mathbb{R}$, the user provide an interval $[a,b]$ such that $x\in [a,b]$ and the composition of interval arithmetical operations, a function $F: I\mathbb{R}\to I\mathbb{R}$, provides the value $F([a,b])=[c,d]$, such that $f(x)\in F([a,b])$. This property is known as interval correctness. In 2006, Santiago and Bedregal investigated it from a topological viewpoint. The result was a method called interval representation, which is a way to define interval functions from real functions. This method has been efficient in applications and in the definition of Fuzzy connectives. The concept of interval and its arithmetic is the basis for the most important definition in Fuzzy theory, however some problems arise because the algebraic structure of intervals. In this talk we discuss some connections between Interval Mathematics and Fuzzy Logic.

Arrow and turnstile interpolations are investigated in UCL (introduced in [SRSM13]), a logic that is  a complete extension of classical propositional logic for reasoning about  connectives that only behave as expected with a given probability. Arrow interpolation is shown to hold in general and turnstile interpolation is established under some provisos. The talk reports on joint work with Amílcar Sernadas and Cristina Sernadas.

A probabilistic logic over equational assertions is proposed in order to obtain a setting able to express security notions that have an intrinsic probabilistic nature and, at the same time, are sensitive to the algebraic properties of cryptographic primitives. Applications are provided in the analysis of security protocols, namely on the existence of off-line guessing attacks and measurement of their success probability.

When studying probabilistic dynamical systems, temporal logic has typically been used to reason about path properties. Recently, there has been some interest in reasoning about the dynamical evolution of state probabilities of these systems. In this paper we show that verifying linear temporal properties concerning the state evolution induced by a Markov chain is equivalent to the decidability of the Skolem problem — a long standing open problem in Number Theory. However, from a practical point of view, usually it is enough to check properties up to some acceptable error bound. We show that an approximate version of Skolem problem is decidable, and that it can be applied to verify, up to an arbitrarily small error, linear temporal properties of the state evolution induced by a Markov chain.

We present a type-based approach to the verification of the communication structure of parallel programs. We model parallel imperative programs where a fixed number of processes, each equipped with its local memory, communicates via a rich diversity of primitives, including point-to-point messages, broadcast, reduce, and array scatter and gather. The theory includes a decidable dependent type system incorporating abstractions for the various communication operators, a form of primitive recursion, and collective choice. We further introduce a core programming language for imperative, message-passing, parallel programming, and show that the language enjoys progress. Joint work with Francisco Martins, Eduardo R.B. Marques, Hugo A. López, César Santos and Nobuko Yoshida.