Events.WorkshopSBL2018 History

Hide minor edits - Show changes to output

Changed lines 26-35 from:
15h30-15h55              Carlos Brito (UFC)\\
16h00-16h40
            Luiz Carlos Pereira (PUC-Rio e UERJ)  (keynote speaker)

16h40-17h00
             Coffee break

17h00-17h25
             João Fernando Lima Alcântara (UFC)\\
17h30-17h55              Marcos Silva (UFAL)\\
18h00-18h25              Samuel G. da Silva (UFBA e SBL)\\
18h30-19h10
              Yiannis Moschovakis  (UCLA e Univ.Athens)  (keynote speaker)
to:
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)
Deleted lines 68-69:
!!! João Fernandes de Lima Alcântara - TBA
Changed lines 75-77 from:
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 - TBA
to:
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.
Changed line 23 from:
14h00-14h25              Mario Benevides (COPPE-UFRJ)\\
to:
14h00-14h25              Mário Benevides (COPPE-UFRJ)\\
Changed lines 25-34 from:
15h00-15h40              Maurício Ayala-Rincón (UnB)  (keynote speaker)\\
15h45-16h10
             Carlos Brito (UFC)\\
16h10-16h35              Luiz Carlos Pereira (PUC-Rio e UERJ)  (keynote speaker)\\
\\
16h35
-17h00               Coffee break\\
\\

17h00-17h25               João Fernando Lima Alcântara (UFC)\\
17h30-17h55               Marcos Silva (UFAL)\\
18h00-18h25               Samuel G. da Silva (UFBA e SBL)\\
18h30-19h10               Yiannis Moschovakis  (UCLA e Univ.Athens)  (keynote speaker)
to:
15h00-15h25              Maurício Ayala-Rincón (UnB)\\
15h30-15h55
            Carlos Brito (UFC)\\
16h00-16h40              Luiz Carlos Pereira (PUC-Rio e UERJ)  (keynote speaker)

16h40
-17h00              Coffee break

17h00-17h25              João Fernando Lima Alcântara (UFC)\\
17h30-17h55              Marcos Silva (UFAL)\\
18h00-18h25              Samuel G. da Silva (UFBA e SBL)\\
18h30-19h10              Yiannis Moschovakis  (UCLA e Univ.Athens)  (keynote speaker)
Changed line 23 from:
14h00-14h25              Mário Benevides (COPPE-UFRJ)\\
to:
14h00-14h25              Mario Benevides (COPPE-UFRJ)\\
Changed line 45 from:
!!! Luiz Carlos Pereira - Gödel's Koan
to:
!!! Luiz Carlos Pereira - Gödel's Koan ([[Attach:WorkshopSBL2018LuizCarlos.pdf|Abstract completo]])
Changed lines 50-51 from:
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.
to:
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.
Added lines 59-64:

!!! 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.
Changed line 56 from:
 * Gentzen’s reduction.
to:
 * Gentzen's reduction.
Changed line 25 from:
15h00-15h40              Luiz Carlos Pereira (PUC-Rio e UERJ)  (keynote speaker)\\
to:
15h00-15h40              Maurício Ayala-Rincón (UnB)  (keynote speaker)\\
Changed line 27 from:
16h10-16h35              TBA\\
to:
16h10-16h35              Luiz Carlos Pereira (PUC-Rio e UERJ)  (keynote speaker)\\
Changed lines 45-58 from:
!!! Luiz Carlos Pereira - TBA
to:
!!! Luiz Carlos Pereira - Gödel's Koan

"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)

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)
Changed lines 38-41 from:
!!!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.

to:
!!! 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 - TBA

!!! 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".

!!! João Fernandes de Lima Alcântara - TBA

!!! 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

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 - TBA

Added line 68:
* Márcia Roberta Falcão de Farias (UNILAB)
Changed lines 38-40 from:
TBA
to:
!!!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.
Changed lines 14-19 from:
Até o momento, temos como  keynote speaker confirmado para o Workshop: Yiannis Moschovakis (UCLA, Califórnia).

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 [[http://lia.ufc.br/~lsfa2018/|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.
to:
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 [[http://lia.ufc.br/~lsfa2018/|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
.
Changed lines 23-34 from:
TBA
to:
14h00-14h25              Mário Benevides (COPPE-UFRJ)\\
14h30-14h55              Umberto Rivieccio (UFRN)\\
15h00-15h40              Luiz Carlos Pereira (PUC-Rio e UERJ)  (keynote speaker)\\
15h45-16h10              Carlos Brito (UFC)\\
16h10-16h35              TBA\\
\\
16h35-17h00              Coffee break\\
\\
17h00-17h25              João Fernando Lima Alcântara (UFC)\\
17h30-17h55              Marcos Silva (UFAL)\\
18h00-18h25              Samuel G. da Silva (UFBA e SBL)\\
18h30-19h10              Yiannis Moschovakis  (UCLA e Univ.Athens)  (keynote speaker)
Changed line 16 from:
     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 [[http://lia.ufc.br/~lsfa2018/|LSFA]] - Logical and Semantic Frameworks, with Applications (26 a 28 de Setembro).
to:
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 [[http://lia.ufc.br/~lsfa2018/|LSFA]] - Logical and Semantic Frameworks, with Applications (26 a 28 de Setembro).
Added lines 1-33:
Attach:Main/sbl.jpg

! 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.

Até o momento, temos como  keynote speaker confirmado para o Workshop: Yiannis Moschovakis (UCLA, Califórnia).

      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 [[http://lia.ufc.br/~lsfa2018/|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.

!! Programação

TBA

!! Resumos das palestras

TBA

!! Organização

* Samuel Gomes da Silva (UFBA e SBL) - Co-chair
* Francicleber Martins Ferreira (UFC) - Co-chair

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.