Seminários 2005.2

• 15/12/2005
  "Extensões Não-Lógicas do Cálculo Relacional",
  por Petrúcio Viana, IM-UFF.
  Resumo:
  Cálculos relacionais são sistemas formais nos quais a informação é expressa em termos de propriedades das relações e a inferência é efetuada através do raciocínio sobre relações. Um de seus mais representativos exemplos é o Cálculo das Relações Binárias, RC. Este sistema, embora adequado para alguns propósitos, tem sérias limitações em seu poder de expressão e prova. Neste seminário, apresentamos extensões de RC, por operadores não-lógicos, no sentido de A. Tarski. Em particular, os seguintes sistemas são abordados: BRC, o cálculo relacional com ligadores; FRC, o cálculo relacional com bifurcação; +RG, o cálculo relacional positivo com grafos; e LTL2, a lógica linear temporal bisortida. Investigamos o poder expressivo de cada sistema e provamos resultados de completude para BRC, FRC, e +RG.
  
  
• 06/12/05
  "A Language for Categorical Semantics: System DNC (III)",
  por Eduardo Ochs, PUC-Rio.
  Resumo (notas do seminário em http://angg.twu.net/seminar-notes.html):
  The category of sets, Set, is a category with some extra structure and properties: it is a topos. Mathematicians usually carry out constructions and proofs inside the class of sets using ZFC, but many of those constructions and proofs can also be expressed in a language a bit weaker than ZFC, called Local Set Theory (LST); constructions and proofs in LST, after a suitable translation to categorical language, can carried out in any topos.
  
  The emphasis of this talk will be on a certain tool for formalizing this. We can express both the (local-)set-theoretic and the categorical constructions in the same language - the language of System DNC -, which makes the translation almost obvious (in a precise sense). The semantics of the "terms" of DNC is apparently tied to Set, but a simple change of dictionary makes the same terms become entities lying in any chosen topos.
  
  
• 01/11/05
  "A Language for Categorical Semantics: System DNC (II)",
  por Eduardo Ochs, PUC-Rio.
  Resumo:
  The category of sets, Set, is a category with some extra structure and properties: it is a topos. Mathematicians usually carry out constructions and proofs inside the class of sets using ZFC, but many of those constructions and proofs can also be expressed in a language a bit weaker than ZFC, called Local Set Theory (LST); constructions and proofs in LST, after a suitable translation to categorical language, can carried out in any topos.
  
  The emphasis of this talk will be on a certain tool for formalizing this. We can express both the (local-)set-theoretic and the categorical constructions in the same language - the language of System DNC -, which makes the translation almost obvious (in a precise sense). The semantics of the "terms" of DNC is apparently tied to Set, but a simple change of dictionary makes the same terms become entities lying in any chosen topos.
  
  
• 20/10/05
  "A Language for Categorical Semantics: System DNC (I)",
  por Eduardo Ochs, PUC-Rio.
  Resumo:
  The category of sets, Set, is a category with some extra structure and properties: it is a topos. Mathematicians usually carry out constructions and proofs inside the class of sets using ZFC, but many of those constructions and proofs can also be expressed in a language a bit weaker than ZFC, called Local Set Theory (LST); constructions and proofs in LST, after a suitable translation to categorical language, can carried out in any topos.
  
  The emphasis of this talk will be on a certain tool for formalizing this. We can express both the (local-)set-theoretic and the categorical constructions in the same language - the language of System DNC -, which makes the translation almost obvious (in a precise sense). The semantics of the "terms" of DNC is apparently tied to Set, but a simple change of dictionary makes the same terms become entities lying in any chosen topos.
  
  
• 11/10/05
  "Decidability of a fragment of the graph calculus for binary relations - part two",
  por Renata P. de Freitas, IM-UFF.
  Resumo:
  In Part One we have presented basic definitions and the graph calculus for binary relations: binary relational terms, models, meaning of a relational term in a model, graph of a relational term, rules for the graph calculus, model induced by a relational term.
  
  In Part Two we will present a witness finite model for valid inclusions in the fragment of the relation calculus where relational terms do not have occurrences of complementation or union. I.e., we will present a construction of a finite model M such that the relation denoted by term R in M is included in the relation denoted by term S in M iff the inclusion between terms R and S is valid, when R and S are relational terms with no occurrences of complementation or union. This implies the decidability of this fragment of the relation calculus. In fact, this fragment of the relation calculus has a truth-table like method of decision: the construction of the witness model to test validity in the relation calculus is analogous to the construction of truth-tables to test validity in the propositional logic.
  
  
• 04/10/05
  "Decidability of a fragment of the graph calculus for binary relations",
  por Renata P. de Freitas, IM-UFF.
  Resumo:
  We present a witness finite model for valid equations in the fragment of the relation calculus where relational terms do not have occurrences of complementation or union. I.e., we present a construction of a finite model M such that the relation denoted by term R in M is included in the relation denoted by term S in M iff the inclusion between terms R and S is valid, when R and S are relational terms with no occurrences of complementation or union. This implies the decidability of this fragment of the relation calculus.
  
  
• 27/09/05
  "Refinamentos não-associativos do Cálculo Lambek" - continuação,
  por Marcelo Corrêa, IM-UFF.
  Resumo:
  No primeiro seminário, apresentamos o Cálculo Lambek, um sistema dedutivo inicialmente concebido para a verificação da boa formação de sentenças em uma certa linguagem natural em termos de uma gramática categorial, e que tornou-se objeto de estudo na área de Teoria da Prova devido às importantes restrições estruturais nele existentes para a obtenção de deduções, ao se considerar sistemas de seqüentes (de Gentzen), por exemplo. Destacamos a caracterização lógica, em termos de um sistema de prova, apresentada para um operador produto tensorial não-comutativo, e possivelmente não-associativo, dependendo das restrições impostas, e os operadores de implicação a ele relacionados. Apresentamos também a motivação para a construção de um sistema lógico intermediário, em comparação com as versões associativa e não-associativa do Cálculo Lambek: a possibilidade de obter um tratamento mais adequado para questões relativas à combinação de expressões, estendendo a linguagem por meio da adoção de um operador que representa o que chamamos de "permissão de combinação" e adotando versões restritivas das regras estruturais de associação.
  
  Neste seminário apresentaremos este sistema intermediário e discutiremos a correlação entre tais sistemas lógicos e as linguagens reconhecidas por gramáticas livres de contexto e questões relativas às gramáticas sensíveis ao contexto.
  
  
• 20/09/05
  "Refinamentos não-associativos do Cálculo Lambek",
  por Marcelo Corrêa, IM-UFF.
  Resumo:
  O Cálculo Lambek, inicialmente concebido como um sistema dedutivo para a verificação da boa formação de sentenças em uma certa linguagem natural em termos de uma gramática categorial, tornou-se objeto de estudo na área de Teoria da Prova devido às importantes restrições estruturais nele existentes para a obtenção de deduções, ao se considerar sistemas de seqüentes (de Gentzen), por exemplo. Destaca-se a caracterização lógica, em termos de um sistema de prova, apresentada para um operador produto tensorial não-comutativo, e possivelmente não-associativo, dependendo das restrições impostas, e os operadores de implicação a ele relacionados.
  Apresentaremos um sistema lógico intermediário, em comparação com as versões associativa e não-associativa do Cálculo Lambek, a fim de obter um tratamento mais adequado para questões relativas à combinação de expressões, estendendo a linguagem por meio da adoção de um operador que representa o que chamamos de "permissão de combinação" e adotando versões restritivas das regras estruturais de associação. Discutiremos também a correlação entre tais sistemas e as linguagens reconhecidas por gramáticas livres de contexto e questões relativas às gramáticas sensíveis ao contexto.
  
  
• 08/09/05, quinta (excepcionalmente)
  "Um diálogo socrático sobre cálculo com grafos para o cálculo das relações binárias",
  por Renata P. de Freitas, IM-UFF.
  Resumo: Apresentação, passo a passo, de um sistema dedutivo usando grafos para o conjunto das equações válidas no cálculo das relações binárias, sem complementação. Este cálculo tem aplicações tanto na fundamentação da matemática quanto na teoria da computação.
  
  
• 30/08/05
  "Problemos fundamentais da combinação de lógicas",
  por Jean-Yves Béziau, Universidade de Neuchatel.