O-minimal structures are the realization of Grothendieck's program of tame topology and generalize semi-algebraic and sub-analytic geometry. In this talk i will describe the recent development of sheaf theory and cohomology theory in this context. These theories have applications ranging from a generalization of Hilbert's 5th problem, homological dimension of sheaves on real analytic manifolds and possibly also a generalization of some results of Suslin-Voevodsky on the algebraic singular homology of varieties over the complex numbers.

Until is a notoriously difficult temporal operator as it is both existential and universal at the same time: $A \cup B$ holds at the current time instant $w$ iff either $B$ holds at $w$ or there exists a time instant $w'$ in the future at which $B$ holds and such that $A$ holds in all the time instants between the current one and $w'$. This "ambivalent" nature poses a significant challenge when attempting to give deduction rules for until. In this paper, in contrast, we make explicit this duality of until by introducing a new temporal operator that allows us to formalize the “history” of until, i.e., the “internal” universal quantification over the time instants between the current one and $w'$. This approach provides the basis for formalizing deduction systems for temporal logics endowed with the until operator. For concreteness, we give here a labeled natural deduction system for a linear-time logic endowed with the new history operator and show that, via a proper translation, such a system is also sound and complete with respect to the linear temporal logic LTL with until. Reporting on joint work with Andrea Masini and Marco Volpe.

In this talk I will present systems of pure modal logics, i.e. with modalities as only connectives. I will focus on alethic modalities: necessity and possibility. The basic framework is structural conesquence relation in the sense of Los and Susko. I will study the main options and present bivalent and multi-valued semantics for these systems as well as sequent-calculi.

Authorization policies are not stand-alone objects: they are used to selectively permit actions that change the state of a system. Thus, it is desirable to have a framework for reasoning about the semantic consequences of policies. To this end, we extend a rewriting interpretation of linear logic with connectives for modeling affirmation, knowledge, and possession. To cleanly confine semantic effects to the rewrite sequence, we introduce a monad. The result is a richly expressive logic that elegantly integrates policies and their effects. After presenting this logic and its metatheory, we demonstrate its utility by proving properties that relate a simple file system's policies to their semantic consequences. This talk represents joint work with Henry DeYoung.

The complexity class DLOGTIME-uniform $\operatorname{AC}^0$ is known to be a modest subclass of DLOGTIME-uniform $\operatorname{TC}^0$. The weakness of $\operatorname{AC}^0$ is due, put in logical terms, to the fact that the logics corresponding to $\operatorname{AC}^0$ do not have the relativization property and hence they are not regular. This weakness of $\operatorname{AC}^0$ has been elaborated in the line of research on the Crane Beach Conjecture. In this talk we show that DLOGTIME-uniform $\operatorname{TC}^0$ can be logically characterized in terms of quantifier logics with cardinality quantifiers $\operatorname{FO}_{\lt}(C_S)$, where $S$ is the range of some polynomial of degree at least two. Then we adapt the key properties of abstract logics to accomodate built-in relations and define the regular interior $R-\operatorname{int}(L)$ and regular closure $R-\operatorname{cl}(L)$, of a logic $L$. Finally we show that the Crane Beach Conjecture can be interpreted as a statement concerning the regular interior of a logic and that the regular closure of $\operatorname{AC}^0$ is $\operatorname{TC}^0$. Joint work with Lauri Hella and Kerkko Luosto.

Capitalizing on the graph-theoretic account of logic systems and their fibrings in [19], and inspired on notions of concurrency, a novel form of combination of logics — parallel composition — is proposed at the semantic level. Parallel composition allows both symmetric (like sharing) and non-symmetric (like triggering) forms of interaction to be specified at the signature level. Parallel composition subsumes fibring as a special case. Parallel composition is presented using universal constructions in the categories of signatures and interpretations, using a cofibration for synchronization. The conservative nature of parallel composition under lossless synchronization is established using a generalized bisimulation technique. The conservative nature of free parallel composition and unconstrained fibring follow as corollaries. Joint work with Cristina Sernadas and João Rasga.

I discuss why consistency may be not absolute, and what is good about this. I argue that a compulsive seeking for just one sense of consistency is hazardous to rationality, and that observing the subtle distinctions of reasonableness between individual and groups may suggest wider notions of consistency, relevant to several areas such as belief revision, logic and even to a re-assessment of Gödel's second incompleteness theorem.

The paper by da Costa and Carnielli “On Paraconsistent deontic logic” (1986) introduced the first modal paraconsistent system, C1D, defined by combining the paraconsistent system C1 and the deontic system D. That paper aimed to show how a paraconsistent deontic system could be used as a new approach for dealing with certain kinds of deontic paradoxes. We call anodic the purely positive versions of modal systems, and cathodic any non-classical (w.r.t. negations) version of modal systems. Paradigmatic examples of the latter are modal paraconsistent systems based upon logics of formal inconsistency (LFIs), i.e., based upon paraconsistent systems where the concept of consistency is internalized within the object language, so as to control the “strength” of negation inside the systems. We discuss here some strategies for obtaining completeness to cathodic systems w.r.t possible-translations semantics, as well as some limitative results concerning incompleteness, emphasizing the role of negation in such constructions.

In this presentation I will propose a general type notation, formal semantics and a sound, compositional, and decidable type system to characterise some liveness properties of distributed systems. In the context of mobile processes, we define two concepts, activeness (ability to send/receive on a channel) and responsiveness (ability to reliably conduct a conversation on a channel), that make the above properties precise. The type system respects the semantic definitions of the concepts, in the sense that the logical statements it outputs are, according to the semantics, correct descriptions of the analysed process. Our work is novel in two aspects. First, since mobile processes can make and communicate choices, a fundamental component of data representation (where a piece of data matches one of a set of patterns) or conversations (where the protocol may permit more than one message at each point), our types and type system use branching and selection to capture activeness and responsiveness in process constructs necessary for such usage patterns. Secondly, conditional properties offer compositionality features that permit analysing components of a system individually, and indicate, when applicable, what should be provided to the given process before the properties hold.

We give a new method to enrich a logic with probability features in the context of a logic systems. Transference of results are addressed, such as completeness, decidability and model-checking. This method will be applied to obtain the probabilization of classic propositional logic (EPPL [P. Mateus, A. Sernadas, and C. Sernadas 2005]) of linear temporal logic (EPLTL), and mu-calculus (MEPL). The complexity of the SAT and model-checking algorithms for theses logics is examined. We briefly discuss how to quantize a logic by a similar process. Part of this work was done in cooperation with P. Mateus and R. Nagarajan.

A formalization of the Turing machines through first-order logic is proposed. In this formalization, Turing machines are defined in terms of first-order structures and, thus, the existence of non-standard elements in Turing machines, similar to those models of first-order arithmetic, is proved. This permits to invesigate some properties of Turing computability over non-standard natural numbers. Finally, some consequences of this approach for important problems related to Turing machines are analised, notably the Máté-Sureson's model-theoretical caracterization of the problem NP=?CoNP.

Verification of probabilistic systems is an active research field due to its wide range of applications. However, the logics usually employed for these purposes (PCTL, PLTL) lack the expressiveness to assert some common requirements. We present an enrichment of the quantified temporal logic originally proposed by Vardi that addresses this problem by allowing reasoning about any semialgebraic constrain over probabilities of paths on Markov chains. We adapt the usual Model Checking techniques to accommodate the increase in expressiveness and devise a SAT algorithm based on Tarski’s result about real algebraic fields. We also present a reduct of this logic that retains much of the expressiveness while having significantly less demanding SAT and MC algorithms. Finally, capitalizing on the SAT, we present a complete Hilbert calculus for the logics. Joint work with M. Biscaia, P. Baltazar and P. Mateus

Bilattices have proven again and again to be extremely rich structures from a logical point of view. As a matter of fact, even if we fix the canonical notion of many-valued entailment and consider the smallest non-trivial bilattice, distinct logics may be defined according to the chosen ontological or epistemological reading of the underlying truth-values. This note will explore the consequence relations of two variants of Belnap’s well-known 4-valued logic, and delve into their interrelationship. The strategy will be that of reformulating those logics using only two ‘logical values’, by way of uniform classic-like semantical and proof-theoretical frameworks, with the help of which such logics can be more easily compared to each other. For a different reading of Belnap’s logic, it will also be proposed a combination mechanism from which it would result in a very natural way.

The purpose of this talk is to show how fusions of modal logics extended with interactive laws can be used to model theories containing interactions of modal concepts. In particular, a combined modal logic – with operators to formalize the notions of imagination, conception and possibility simultaneously – is explored and developed.

In this talk we deal with logics with negation as the only connective. We study the relations between the main properties of pure negation and the various ways to define classical negation. We also study intuitionistic negation and minimal negation. We explain then how we can combine these different logics of negation with each other and with other pure logics: pure alethic modal logic, pure logics of conjunction, disjunction, implication. To develop this study we are using structural consequence operators, sequents systems and bivaluations.

A well-known result by Palamidessi tells us that $\pi_\text{mix}$ (the $\pi$-calculus with mixed choice) is more expressive than $\pi_\text{sep}$ (its subset with only separate choice). The proof of this result argues with their different expressive power concerning leader election in symmetric networks. Later on, Gorla offered an arguably simpler proof that, instead of leader election in symmetric networks, employed the reducibility of “incestual” processes (mixed choices that include both enabled senders and receivers for a common channel) when running two copies in parallel. In both proofs, the role of breaking (initial) symmetries is more or less apparent. In this talk, we shed more light on this role by re-proving the above result|based on a proper formalization of what it means to break symmetries — without referring to another layer of the distinguishing problem domain of leader election. Both Palamidessi and Gorla rephrased their results by stating that there is no uniform and reasonable encoding from $\pi_\text{mix}$ into $\pi_\text{sep}$. We indicate how the respective proofs can be adapted and exhibit the consequences of varying notions of uniformity and reasonableness. In each case, the ability to break initial symmetries turns out to be essential.