October 13th, 2015
Universidade Federal Fluminense
Insituto de Computação
Av. Gal. Milton Tavares de Souza, s/n
Niterói - RJ
|8:50h-9:10h||::||Edward Hermann Haeusler|
Abstract. Reasoning about concurrent programs is much harder than reasoning about sequential ones. Programmers often find themselves overwhelmed by the many subtle cases of thread interactions they must be aware of to decide whether a concurrent program is correct or not. In this talk I will introduce Saraswat's Concurrent Constraint Programming (CCP), a declarative model of concurrency where agents can be seen, coherently, as (concurrent) processes and formulas in logic. The core CCP language can be extended to deal with different modalities (e.g., temporal, spatial and epistemic modalities) as well as with preferences (e.g., probabilities, fuzzy information, etc.). By giving a logical characterization of such modalities, we show that CCP's extensions are not ad-hoc. More precisely, we can exhibit a tight adequacy result between operational steps in the (extended) CCP language and derivations in linear logic with subexponentials (SELL). Moreover, by studying the proof theory of SELL, we show how to define new declarative constructors for CCP. Hence, SELL is not only a framework for verifying CCP programs but it is also useful to enrich the language of processes to cope with more interesting behaviors in concurrent systems.
Abstract. Several resolution-based methods have been designed to deal with the satisfiability problem in modal logics. As its classical counterpart, those methods often follow a pure syntactical approach and rely on heavy preprocessing of the formulae being tested for satisfiability. In this talk, we give an overview on how such calculi can be enriched with semantic annotation and discuss some aspects related to the effectiveness and efficiency of the resulting calculi.
Abstract. We discuss some aspects related to the computational complexity of propositional logics and the feasiability of automated theorem proving.
Abstract. We propose a notion of focusing for nested sequent calculi for modal logics which brings down the complexity of proof search to that of the corresponding sequent calculi. The resulting systems are amenable to specifications in linear logic. Examples include modal logic K, a simply dependent bimodal logic and the standard non-normal modal logics. As byproduct we obtain the first nested sequent calculi for the considered non-normal modal logics.
Abstract. We study effectiveness in the domain of computability. In the context of model-theoretical approaches to effectiveness, where a function is considered effective if there is a model containing a representation of such function, our definition relies in a model provided by functions between finite sets and uses category theory as its mathematical foundations. In our model we use the fact that every function between finite sets is computable, and that finite composition of such functions is also computable. Our approach is an alternative to the traditional model-theoretical based works which rely on (ZFC) set theory as a mathematical foundation, and our approach is also novel when compared to the works using category theory to approach computability results.
Abstract. This is a short comparison of some important consequences of sequent calculus and natural deduction formalisms to logic and computer science.
Abstract. It is proposed a new Epistemic logic aimed to reasoning about authentication and secrecy in communication protocols. The logic is based on Dolev Yao model for analyzing security of public key protocols. It is presented an axiomatization and proofs of soundness and completeness. In oder to illustrate the applicability of this new logic it is verified some examples and some well known protocols (Keberos and RPC). Finally, the logic is extended with common knowledge operator and again a sound and complete axiomatization is provided.
Abstract. We define the quasi-equational and Horn-quasi-equational theories of residuated algebras of binary relations. We review some negative results showing that these theories are not finitely axiomatizable (on the top of equational logic). We present two alternatives for proving the valid quasi-equations and Horn-quasi-equations: Calculational Reasoning and Diagrammatic Reasoning. We close by discussing some open problems relating these environments. This is a joint work with Marcia Cerioli (IM/COPPE/UFRJ).
Bruno Lopes (IC/UFF)