II Workshop da Sociedade Brasileira de Lógica

Informações importantes

  • Local: Departamento de Computação - Campus do PICI, UFC (Fortaleza-CE)
  • Data: 28 de setembro de 2018, 14:00h

Sobre o evento

O II Workshop da Sociedade Brasileira de Lógica é uma iniciativa da Sociedade Brasileira de Lógica - SBL, consistindo de palestras e comunicações convidadas, com o objetivo de apresentar um painel da pesquisa em Lógica no Brasil (e em particular, no Nordeste), em todas as suas vertentes: Filosofia, Ciência da Computação, Matemática.

Os keynote speakers do Workshop serão: Yiannis Moschovakis (UCLA, Califórnia) e Luiz Carlos Pereira (PUC-Rio e UERJ).

O Workshop realiza-se no Departamento de Ciência da Computação, Campus Pici, na mesma semana em que ocorre em Fortaleza uma edição do tradicional evento LSFA - Logical and Semantic Frameworks, with Applications (26 a 28 de Setembro).

O Workshop é isento de inscrição. As informações sobre credenciamento no evento LSFA podem ser verificadas no próprio site do evento. Todas as apresentações do Workshop serão em inglês.

Programação

14h00-14h25 Mário Benevides (COPPE-UFRJ)
14h30-14h55 Umberto Rivieccio (UFRN)
15h00-15h25 Maurício Ayala-Rincón (UnB)
15h30-16h10 Luiz Carlos Pereira (PUC-Rio e UERJ) (keynote speaker)\\

16h10-16h30 Coffee break

16h30-16h55 Carlos Brito (UFC)
17h00-17h25 Marcos Silva (UFAL)
17h30-17h55 Samuel G. da Silva (UFBA e SBL)
18h00-18h40 Yiannis Moschovakis (UCLA e Univ.Athens) (keynote speaker)

Resumos das palestras

Mario Benevides (COPPE-URFJ) - Propositional Dynamic Logic for Bisimilar programs with Parallel Operator and Test

Abstract: In standard Propositional Dynamic Logic (PDL) literature, the semantics is given by Labeled Transition Systems, where for each program π we associate a binary relation Rπ. Process Algebras also give semantics to process (terms) by means of Labeled Transition Systems. In both formalisms, PDL and Process Algebra, the key notion to compare processes is bisimulation. In PDL, we also have the notion of logic equivalence, that can be used to prove that π1 and π2 are logically equivalent ⊢ ⟨π1⟩φ ↔ ⟨π2⟩φ. Unfortunately, logic equivalence and bisimulation do not match in PDL. Bisimilar programs are logic equivalent but the converse does not hold. In this talk we present a semantics and an axiomatization for PDL that makes logically equivalent programs also bisimilar. This allows for developing Dynamic Logics to reasoning about process algebra specifications, in particular about CCS (Calculus for Communicating Systems). As in CCS, bisimulation is the main tool to establish equivalence of programs, it is very important that these two relations coincide. We propose a new Propositional Dynamic Logic with a new non-deterministic choice operator, PDL+. We prove its soundness, completeness, finite model property and EXPTIME-completeness for the satisfiability problem. We also add to PDL+ the parallel composition operator (PPDL+) and prove its soundness and completeness. We establish that the satisfiability problem for PPDL+ is in 2-EXPTIME. Finally, we define some fragments of PPDL+, prove its EXPTIME-completeness and discuss some issues concerning test operator and point out some direction on how it can be handled.

Umberto Rivieccio - Dualities for two-sorted lattices

Abstract: Duality theory is an attempt at understanding algebras (of logic) via topological methods. For algebras related to logic, the earliest and most important result in this field is M. Stone’s representation of Boolean algebras via certain compact Hausdorff spaces today known as Stone spaces. A new perspective was brought into duality theory by H. Priestley, who introduced ordered topological spaces (Priestley spaces) to give an elegant representation of distributive lattices and related structures. Nowadays the results of Stone and Priestley have been extended in several directions, obtaining dualities for many classes of algebras related to logic: modal algebras, Heyting algebras (algebras of intuitionistic logic), MV-algebras (Lukasiewicz many-valued logic) as well as more esoteric algebras of non-classical logic. As I will show, some of these can be presented as many-sorted structures in a way that has proved quite insightful. In particular, it makes it possible to adapt straightforwardly the results of Stone and Priestley to obtain neat dualities for a variety of non-classical algebras.

Luiz Carlos Pereira - Gödel's Koan (Abstract completo)

"A koan is a story, dialogue, question, or statement, which is used in Zen practice to provoke the 'great doubt' and test a student's progress in Zen practice." (Wikipedia)

Abstract: In 1968 William Howard proposed an assignment of ordinals less than epsilon zero to terms for primitive recursive functionals of finite type with the property that the reduction of a term always lowers its ordinal measure. In a certain sense, it was Howard’s assignment that motivated the appearance in 2014 of problem 26 (submitted by Henk Barendregt) in the TLCA list of open problems, the so-called Gödel's Koan.

The aim of this paper is to explore three different routes to the solution of Gödel's Koan:

 * Disatrous derivations;
 * Mimpgraphs; and
 * Gentzen's reduction. 

(joint work with Edward Hermann Haeusler, PUC-Rio, e Daniel Durante, UFRN)

Mauricio Ayala-Rincón - Termination of Rewriting Systems and Recursive Functions

Abstract: Termination is a fundamental logical property of great interest in computability that despite the well-known fact of being undecidable has given rise to the development of several semi-decision technologies, by its relevance in specification, verification and programming. The talk will focus in the adaptation of the criterion known as Dependency Pairs, originally developed to check termination of term rewriting systems,  to the formal verification of this property for functional specifications.

Joint work with Ariane Alves, César Muñoz and Mariano Moscato.

Carlos Brito - Languages, Tools and Machines

Abstract: The representationalist paradigm, as well as the pragmatist paradigm of the philosophy of language are based on some notion of knowledge: the first on the notion of "know that" and the second on the notion of "know how". In this talk, we are going to investigate situation where the use of language does not rely on any notion of structured knowledge whatsoever --- which lead us to a new paradigm for the philosophy of language based on the idea of "not knowing".

Marcos Silva - Revision of logic: a pragmatist proposal

Abstract: How can we rationally justify our logical principles if the very possibility of rational justification presupposes them? How can we use reason to ground a set of basic principles of reason as the correct one without circularity or any infinite regress? My proposal aims at developing some tenets presented in Wittgenstein’s On Certainty by offering an integrated pragmatist view about the possibility of non-classical logics and logical pluralism. I then apply Wittgenstein’s hinge epistemology and his anti-realism into the discussion about rival logics. Accordingly, I reject a realist approach to logic and propose a view in which the nature of logical principles is related to Moorean propositions. I aim to show that, if logical principles are to be taken as Moorean propositions, we have to acknowledge the role that education, institution, and conversion play in our inferential practices.

Samuel G. da Silva - The Axiom of Choice and the Partition Principle from Dialectica Categories

Abstract: The method of morphisms is a well-known application of Dialectica categories to Set Theory (more precisely, to the theory of cardinal invariants of the continuum). In a previous work, Valeria de Paiva and the author have asked how much of the Axiom of Choice is needed in order to carry out the referred applications of such method. In this paper we show that, when considered in their full generality, those applications of Dialectica categories give rise to equivalents (within ZF) of either the Axiom of Choice (AC) or of the Partition Principle (PP) – which is a consequence of AC whose precise status of its relationship with AC itself is an open problem for more than a hundred years.

Yiannis Moschovakis - A survey of the origins and development of Descriptive Set Theory

Abstract: The central problem of Descriptive Set Theory was posed by Henri Lebesgue in a classic 1905 article: to identify and study the properties of those sets and functions on the real numbers which are "analytically definable". Today we recognize Lebesgue's paper as one of the first important contributions to the "theory of definability", especially as it led in time into a broa study of "first order definability over the real numbers".

My aim in this expository talk is to outline the history of this field which has important applications (especially to analysis) but also interacts substantially with the general theory of sets, logic and even computability theory; I will assume some basic knowledge of these fields but no special knowledge of Descriptive Set Theory.

Organização

  • Samuel Gomes da Silva (UFBA e SBL) - Co-chair
  • Francicleber Martins Ferreira (UFC) - Co-chair
  • Márcia Roberta Falcão de Farias (UNILAB)

Obs.: Por uma coincidência, as duas primeiras edições do Workshop da SBL (2017 e 2018) tiveram como sede escolhida uma cidade do Nordeste brasileiro. A SBL está aberta a propostas de realizações de Workshops em outras regiões do país, sempre buscando aproveitar a presença de pesquisadores de Lógica numa determinada cidade em decorrência da realização de algum evento maior.