After a brief overview of the topic, the concept of fibring is extended to higher-order logics with arbitrary modalities and binding operators. A general completeness theorem is established for such logics including HOL and with the meta-theorem of deduction. As a corollary, completeness is shown to be preserved when fibring such rich logics. This result is extended to weaker logics in the cases where fibring preserves conservativeness of HOL-enrichments. Soundness is shown to be preserved by fibring without any further assumptions.

Neural Networks with the saturated linear activation function are known to be Turing universal. The question on whether the same result holds for networks with a sigmoid activation function is a controversial one amongst the scientific community. The main aim of this talk is to shed some light into the question. It will be shown that Turing machines can be simulated by alarm clock machines, via the introduction of counter machines and adder machines. Next, a description will be given of how to substitute the alarm clocks by restless counters (which can be implemented by sigmoidal neurons). Finally, the simulation of alarm clock machines with restless counters by sigmoidal neural networks will be broken down into parts and analyzed.

Real recursive functions are defined similarly to the classical case, with the difference that we take functions defined on the reals. Although apparently different, several connections between these two approaches are known to exist. In this talk, we further extend those connections. In particular, we define new classes of real recursive functions and relate them with the classes of primitive recursive, recursive and partial recursive functions. We also present an analog of the Arithmetical Hierarchy for the real case and establish connections between the two. Some considerations on the limitations of this kind of connections are also taken in account. Finally, we establish links between real recursive functions and analog circuits.

The main aim of the talk is to propose a new perspective under which branching-time can be investigated. In a tree-like representation of time, the set of histories can be endowed with a topological structure, allowing a topological characterization of basic notions in branching-time semantics. For instance, bundles are dense sets of histories, and a bundle is minimal if and only if the topology induced on it is the discrete topology. Moreover, it will be shown that there is a natural correspondence between non-archimedean topological spaces and bundled trees and that the notions of validity w.r.t. the two kinds of structures coincide.

Recentemente tem sido apontada a natureza caótica de sinais observados no cérebro humano e no de outros animais. A presença de caos parece proporcionar as condições para que certas formas de processamento computacional sejam possíveis. O paradigma caótico é por nós explorado quando trazido para sistemas de computação formal. Os algoritmos e arquitectura por nós adoptados em redes neuronais permanecem próximos da biologia. As redes têm uma distribuição espacial e apresentam uma dinâmica não trivial. Uma das dificuldades técnicas associadas a sistemas caóticos espácio-temporais é a do seu eventual controlo. No nosso caso, esse controlo é indispensável para que a computação seja possível de todo. Este e outros aspectos técnicos levam a uma incursão na área dos Sistemas Dinâmicos. A computação surge no contexto da classificação de padrões, sendo enfatizado o papel das simetrias espácio-temporais.

Quantum entanglement is a subtle nonlocal correlation among the parts of a quantum system that has no classical analog. Thus entanglement is best characterized and quantified as a feature of the system that cannot be created through local operations that act on different parts separately, or by means of classical communication among the parts. One application of shared entanglement is a novel quantum communication protocol called quantum teleportation. To teleport a qubit (quantum bit) the receiver needs to receive two classical bits in order to recover the perfect replica. This protocol has been convincingly demonstrated in the laboratory.

Finite Automata are commonly used in Hybrid Systems, however these are frequently continuous time systems while the classical finite automata theory deals with discrete time. The main objective of this talk is to lift basic concepts of automata theory from discrete to continuous time. Functions computed by finite automata will be considered rather than the sets accepted by these and examples of such devices over non-Zeno signals will be given. At last, a function algebra for a special class of functions over non-Zeno signals will be discussed and some examples of circuits given.

The notion of LDFOB logic is revised in order to use formulae as the basic unit of reasoning (instead of judgements) and to incoporate freshness conditions in provisos. A completeness theorem is established encompassing a suitably large class of such logics. Several interesting examples are discussed. The fibring of such logics is sketched.

The specifications of electronic money protocols usually presented in the literature consist of informal descriptions of message flows. Therefore, it seems essential to develop a formalism to specify and verify such protocols. To this end, we start by sketching an enrichment of the spi-calculus encompassing the notion of state. Using this formalism, we specify an electronic money protocol. In order to show that this protocol is secure against e-coin replication in the presence of private and authenticated channels, we first introduce a notion of equivalence between agents and explore its main properties. Indeed, the protocol is shown to be secure by proving that it is equivalent to an ideal perfect protocol. Finally, we also show how to emulate private and authenticated channels using public channels and cryptography.

One of the main goals of formalizing mathematics is to develop automation strategies/tactics that prove (partial) goals without requiring any input from the user. In this talk we show how to achieve this desideratum for the domain of real analysis in the proof assistant Coq, by defining ever more powerful tactics through two different strategies: the Auto with Hints mechanism and the use of Reflection.

This talk will identify and explore some applications for proof-theoretic methods from logic to computer security, the branch of computer science concerned with the protection of computer systems and digital information. While cryptography is a well-developed area with a sound mathematical basis, many practical computer security problems involve failures of software design and implementation, not failures of cryptography. The areas of network security, access control, intrusion detection, and system security are full of informal practices waiting to be given precise definitions and analyzed. This talk will discuss a rigorous and precise framework, based on logic, for an analysis of network security protocols that are commonly used to protect access to computer systems and to protect transactions over the internet.

Society Semantics, introduced by W. Carnielli and M. Lima-Marques, is a method for obtaining new logics from the combination of agents (valuations) of a given logic. The goal of this talk is to present several generalizations of this method, as well as to show some applications to many-valued logics. After a reformulation of Society Semantics in a wider setting, we develop two examples of application of the new formalism, characterizing a hierarchy of paraconsistent logics called $P^n$ (for every natural number $n$) and a hierarchy of paracomplete logics $I^n$ (for every natural number $n$). We also propose three increasing generalizations, obtaining Society Semantics for several many-valued logics, including a hierarchy of logics called $I^nP^k$ which are both paraconsistent and paracomplete.

Tableaux are a very convenient tool for proofs in classical and non-classical logics, since proof arguments are analyzed instead of synthesized. This seems to be much closer to human reasoning, and to the way humans specify machine reasoning. In this way, tableau methods are much superior than hilbertian methods or natural deduction for software checking, relational and deductive databases and knowledge representation. Tableaux are also philosophically appealing, as they break down the purported duality between syntax and semantics. In many situations, however, natural deduction, sequents and tableau methods can be inter-translated. In this talk I intend to discuss some aspects of such questions and to sketch a general theory of tableau completeness applicable to several non-standard logics and their combinations.

I introduce the on-the-fly model-checker OFMC, a state-of-the-art tool for analyzing security protocols. For example, OFMC can find attacks in a test-suite consisting of 36 well-known flawed protocols in less than a minute of total CPU time. To our knowledge, there is no other tool for finding attacks that is this fast and has comparable coverage. I will also report on a new attack on the Yahalom protocol found by our tool. OFMC owes its success to the combination of two ideas. The first is the modeling of protocols using lazy data-types in a higher-order functional programming language, which allows for the automated analysis of security properties using infinite-state model checking, where the model is explicitly built, on-the-fly, in a demand-driven fashion. The second is the integration of several search optimizations that significantly reduce the infinite search tree associated with a protocol without excluding any attacks. OFMC was developed in the context of the AVISS project, which developed a tool for security protocol analysis that supports the integration of back-ends implementing different search techniques, allowing for their systematic and quantitative comparison and paving the way to their effective interaction.

In the general context of the theory of institutions, several notions of parchment and parchment morphism have been proposed as the adequate setting for combining logics. However, so far, they seem to lack one of the main advantages of the combination mechanism known as fibring: general results of transference of important logical properties from the logics being combined to the resulting fibred logic. In previous work, we have proposed a setting for bringing fibring to the realm of institutions through the novel notion of c-parchment, and managed to prove several soundness and completeness preservation results for propositional-based logics. Herein, we extend these results to c-parchments also encompassing logics with variables, terms and quantifiers. As a working example we look into modal first-order logic as a fibring of modal propositional logic and first-order logic, and compare the results with several of the alternative semantics proposed in the literature.

We give an alternative axiomatization of Freyd's paracategories, which can be interpreted in any bicategory of partial maps. Assuming furthermore a free-monoid monad $T$ in our ambient category, and coequalisers satisfying some exactness conditions, we give an abstract envelope construction, putting paramonoids (and paracategories) in the more general context of partial algebras. We introduce for the latter the notion of saturation, which characterises those partial algebras which are isomorphic to the ones obtained from their enveloping algebras. We also set up a factorisation system for partial algebras, via inclusions and Kleene morphisms. We also explore some of the global aspects of the category of paracategories — (co)completeness and cartesian closure. We set-up the relevant notion of adjunction between paracategories, illustrated by the cartesian-closed paracategory of bivariant functors and dinatural transformations.

We provide an operational semantics based on finite automata for the language of quiescent and guarded process terms presented by Costa and Sernadas in 1995. For each process there is a finite automaton that embodies the concepts of terminal and non-terminal states through the distinction between terms that denote processes in a quiescent (terminal) state and terms that denote processes in an active state (non-terminal). A rollback mechanism is also provided by transitions of "undo" actions from active states to another state (active or passive). The behaviour of a process is captured by a subset of the language recognised by the respective automaton. A relation of partial order between process terms is defined in order to prove full abstraction in this semantics for the closed terms of the language. Thus, we complete the Hennessy’s trinity, together with the denotational and the axiomatic semantics already introduced by Costa and Sernadas.

We give a general introduction to the problem of computation in groups and define logical graphs for formal proofs. Then, we present the notion of distorsion for finitely presented groups, and show how this phenomena is recaptured by the process of cut-elimination in formal proofs.

In this talk I will introduce hybrid logics, an extension of modal logics which permits explicit reference to the elements of the model. We will focus on the hybrid languages H(@) and H(@,¯) and their temporal extensions, discussing expressive power, complexity of their satisfiability problem and some meta-logical properties like interpolation. The results I will present will help exemplify some of the special techniques (i.e. spy point arguments) characteristic to hybrid languages.

Knots are embeddings of $S_1$ into $3$-space and are classified modulo isotopy. Knot theorists have always been concerned with finding new ways of telling knots apart. In his PhD thesis, D. Joyce defined, for each knot, an algebraic gadget called knot quandle and proved it to be a classifying invariant for knots. In this way, the set of quandle homomorphisms (known as colorings) from the knot quandle to a given (labelling) quandle is also an invariant. We consider an apparently innocuous invariant, counting colorings, and illustrate its effectiveness on telling apart knots of up to and including ten crossings. In this talk we will go over these issues as well as introduce the CJKLS invariant, a knot invariant whose basic ingredients are quandle cohomology and colorings.

Although quite powerful, the fibring mechanism for combining logics suffers from an anomaly usually known as "the collapsing problem". In the first accounts of fibring it could be noticed that fibring a 2-valued with a 3-valued logic would yield no fibred 3-valued models, or that the fibring of classical with intuitionistic logic would collapse into just classical logic. The source of the problem, a too strict identification of truth-values, was also the reason why the classes of models of logics being fibred were required to fulfill some closure properties. In [Sernadas, Rasga and Carnielli] modulated fibring has been introduced and shown to avoid these collapses, by means of a careful use of adjunctions between lattice structured models. In this work, we propose a structurally simpler alternative to solve the semantic collapse problem, by adopting a more general notion of fibred semantics using cryptomorphisms, in a spirit similar to the mechanisms for combining parchments in the theory of institutions. In particular, we show that the novel notion of cryptofibring encompasses the original definition of fibred model, while admiting also (initial) amalgamated models that can be used to show that the above mentioned collapses are no longer present. This talk is on ongoing joint work with A. Sernadas and C. Sernadas.

In this sequel to Counting Colorings of Knots we will discus two ways of representing knots — Burau matrices and Gauss codes — and how to implement, from each of them, algorithms for listing colorings. Clarifying examples will be given. We will also briefly address the one-dimension higher problem of coloring knotted surfaces.

Operads describe a variety of algebraic structures and are particularly useful to organize hierarchies of higher homotopies. In some cases, it is required to relax the notion of operad by specifying domains of composable elements, which leads to the notion of partial operad. Two significant examples are considered: vertex operator algebras and partial operads on configuration spaces of points in a Riemannian manifold. Our approach is to define partial operads as paramonoids, exploring the fact that operads are monoids. Thus, we expect that the theory of paramonoids can be used to generalize operadic completion results, such as the Axelrod-Singer compactification. This talk is on ongoing joint work with C. Hermida.

Approximations are used for dealing with problems that are hard. In this talk, we introduce the concepts relating to the approximation of Propositional Classical Logic with a family of Logics. We do not deal with logics that give answers “approximately correct” such as Fuzzy or Multivalued Logics, but with families of logics that, in the limit, tend to Classical Logic. It also happens that approximated reasoning plays an important role in modelling non-ideal agents. Real agents (natural or artificial) are limited in their reasoning capabilities. We present a general framework for modelling limited reasoning based on approximate reasoning and discuss its properties. The original ideas from which this approach developed were proposed by Cadoli and Schaerf. Unfortunately, their proposal had limitations, both in the expressivity of the language as well as in the inexistence of an incremental method to perform the approximations. Our work has focused on solving these defficiencies, and in understanding some interesting phenomena that we uncover in this process, such as the balance between expressivity vs control of approximations. Some open problems and discussed at the end.

We define a language whose type system allows complex protocols to be specified by types. Our formulation is based on the lambda-calculus with side-effecting input/output operations, where typing judgements describe dynamic changes in the type of channels, channel types track aliasing, and function types describe changes in channel types. This talk is on ongoing joint work with A. Ravara and S. Gay.