Natural deduction systems are historically and conceptually connected to assumption formation. Proofs are defined as derivations where all assumptions are discharged. In Prawitz’ Natural Deduction the systems for classical, intuitionistic and minimal logic are first defined with no discharging strategy (or with the so-called “savage” discharging strategy). Discharging functions were not used before the chapter devoted to modal logic. We know that although there is no difference in deductive power, the adoption of no discharging strategy/function has undesirable proof-theoretical consequences:

[a] No strong normalization; [b] No unicity of normal form; [c] No Curry-Howard.

The aim of this presentation is twofold:

[1] To examine the general role of dependency relations and discharging functions in proof-theory.

[2] (together with E, Hermann Haeusler) In a recent [still unpublished] paper, Prawitz was able to use, “in a seemingly magical way”, the techniques introduced by Gentzen in the second consistency proof in order to prove a normalization theorem directly for a natural deduction formulation of Peano’s Arithmetic. Prawitz’s proof solved a problem that resisted a satisfactory solution for more than 35 years: how to extend Gentzen’s proof to natural deduction, in particular, how to define the notion of level line, so fundamental in the case of sequent calculus, directly for natural deduction. Our second aim is to explore the way Prawitz’ result deals with the problem of assumption-substitution in order to obtain a new proof of strong normalization. 

In this talk we start by describing weakly extensional Heyting arithmetic in all finite types. We then present Gödel's functional or ‘dialectica’ interpretation of arithmetic, and discuss its soundness proof and the circumstances in which a formula is equivalent to its interpretation.

Fibring is a powerful mechanism for combining logics, and an essential tool for designing and understanding complex logical systems. Given two logic systems L1 and L2, their fibring L1 • L2 is the smallest logical system for the combined language which contains both L1 and L2. From the point of view of Hilbert systems, this corresponds precisely to putting together the Hilbert systems of the two logics, allowing instantiations with formulas in the joint signature along the derivations. In this presentation we give a full characterization of the consequence relation that emerges from fibring in the particular case where the logics being combined do not share any connectives. We show the power of this tool by presenting various applications on important problems regarding combined logics: (1) conservativity, (2) decidability and complexity, and (3) the preservation of many-valuedness. Joint work with C. Caleiro.

We analyze the GenPSAT problem, which is an extension of the probabilistic satisfiability problem to linear combinations of probabilistic propositional formulas. GenPSAT is shown to be NP-complete and a reduction to the Mixed Integer Programming problem is explored. Furthermore, we present a GenPSAT solver and analyze the presence of phase transition behaviour. This is joint work with Filipe Casal and Carlos Caleiro.

This talk is about reachability problems for continuous linear dynamical systems. A central decision problem in this area is the Continuous Skolem Problem, which asks whether a real-valued function satisfying an ordinary linear differential equation has a zero. This can be seen as a continuous analog of the Skolem Problem for linear recurrence sequences, which asks whether the sequence satisfying a given recurrence has a zero term. For both the discrete and continuous versions of the Skolem Problem, decidability is open. We show that the Continuous Skolem Problem lies at the heart of many natural verification questions on linear dynamical systems, such as continuous-time Markov chains and linear hybrid automata. We describe some recent work that uses results in transcendence theory and real algebraic geometry to obtain decidability for certain variants of the problem. In particular, we consider a bounded version of the Continuous Skolem problem, corresponding to time-bounded reachability. We prove decidability of the bounded problem assuming Schanuel's conjecture, one of the main conjectures in transcendence theory. We describe some partial decidability results in the unbounded case and discuss mathematical obstacles to proving decidability of the Continuous Skolem Problem in full generality. This is joint work with Ventsislav Chonev and Joel Ouaknine.

This talk will look at non-classical negations and their corresponding adjustment connectives from a modal viewpoint, over complete distributive lattices, and apply a very general mechanism in order to offer adequate analytic proof systems to logics that are based on them. Defining non-classical negations within usual modal semantics automatically allows one to treat equivalent formulas as synonymous, and to have a natural justification for a global version of the contraposition rule. From that perspective, our study offers a particularly useful environment in which negative modalities and their companions may be used for dealing with inconsistency and indeterminacy. After investigating modal logics based on arbitrary frames, we extend the results to serial frames, reflexive frames, and functional frames. In each case we also investigate when and how classical negation may thereby be defined. This reports on joint work with Ori Lahav and Yoni Zohar.

The main classification of sentential logics in Abstract Algebraic Logic (AAL) is the so-called Leibniz hierarchy. It has its roots in the seminal work of Blok and Pigozzi on algebraizable logics, and it classifies a given logic according to algebraic properties of the Leibniz operator over the logical filters. In this talk we shall focus on the less-known Suszko operator, introduced by Czelakowski, which seems to play a more significant rôle when dealing with non-protoalgebraic logics. We present some recent developments in AAL arising from this shifting of paradigm-operator. Namely, we characterize the main classes of logics within the Leibniz hierarchy through algebraic properties of the Suszko operator, and present new isomorphism theorems for protoalgebraic and equivalential logics, in the same spirit of the known ones for weakly-algebraizable and algebraizable logics. This is a joint work with Ramon Jansana and Josep Maria Font.

Belnap-Dunn logic is a well-known four-valued logic that has been widely applied in computer science since its introduction forty years ago. From an algebraic logic point of view, it is an interesting and natural example of a non-protoalgebraic logic. I will take a look at extensions (i.e. stronger logics, but in the same language) of this logic. The final aim would be to describe their hierarchy and providing axiomatizations for (some of) them. However, major difficulties in accomplishing this stem from the fact that (1) most super-Belnap logics are themselves non-protoalgebraic and (2) there are (at least) uncountably many of them.

In this talk we present a new generalization of the mathematical notion of distance. It is based on the abstraction of the codomain of the distance function. The resulting functions must satisfy a generalized triangular inequality, which depends only on the order structure of the valuation space, i.e., a monoid structure is not required. This type of function will be called i-Distance (i-metric, i-quasi-metric, etc). We show that they generate a topology in a very natural way based on open balls. This concept has been successfully applied in the field of Clustering Algorithms and Pattern Recognition. We show how the concept was applied in this field as well as some theoretical results.

There are several operators related to fuzzy logic which in general are generalization of classical ones. For instance, triangular norms and conorms (t-norms and t-conorms for short) generalize the operators "and" and "or" from classical logic. A natural question arises: Without loss of generality if we consider a t-norm T defined on a sublattice M of bounded lattice L which satisfies a property P is it possible (1) to extend T to a function T' on L in such way that T' is also a t-norm and (2) T' also satisfy the property P. In this talk we present two different methods for extending t-norms, t-conorms, fuzzy negations and implications (namely, extension via retractions and extension via e-operators) from a sublattice to a lattice considering a generalized notion of sub lattices. For both methods goal (1) is completely achieved, however extension via retractions fails in preserving some properties of these fuzzy connectives.

In this talk I will discuss systems of sequents with only one formula on the right and one formula on the left. I will compare these systems with other ones (standard systems, intuitionist and dual intuitionist sequent systems), and show how we can generalize known results, in particular cut-elimination, to this framework. I will also study some specific cases/applications of monosequents such as non-distributive logics.

Two fundamental results of classical automata theory are the Kleene theorem and the Buchi-Elgot-Trakhtenbrot theorem. Kleene's theorem states that a language of finite words is definable by a regular expression iff it is accepted by a finite state automaton. Buchi-Elgot-Trakhtenbrot's theorem states that a language of finite words is accepted by a finite-state automaton iff it is definable in the weak monadic second-order logic.

Hence, the weak monadic logic and regular expressions are expressively equivalent over finite words. We generalize this to words over arbitrary linear orders.

Choreographies are widely used for the specification of concurrent and distributed software architectures. In previous work, we proposed Core Choreographies (CC), a model for investigating foundational questions in choreography calculi. In this talk, we discuss two such questions: asynchrony and behaviour extraction.

Asynchronous communications are ubiquitous in real-world systems, and we show how it can be modeled either by endowing CC with a different semantics or by minimally extending its syntax and implementing message queues. Since CC is a core model, these constructions can be generalized to most choreography languages.

Extraction concerns the issue of deciding whether the behaviour of a given process network can be expressed as a choreography, and if possible finding this choreography. In general, these questions are undecidable; we show that in CC we can find algorithms to answer them.