Universidade do Minho  

           
 
  Autenticação/Login
 
Contacts
Site Map
   
  print
 
back 
Construção automática de provas e de contra-modelos em lógica proposicional bi-intuicionista

A lógica bi-intuicionista é uma extensão da lógica intuicionista com um conectivo dual à implicação (relacionado com a diferença de conjuntos), que admite interpretações em termos de estruturas de Kripke e de álgebras de Heyting-Brouwer.
O cálculo proposicional desta lógica é decidível, mas não são conhecidas formulações convencionais de cálculo de sequentes com a propriedade da eliminação do corte que o caracterizem, pelo que o desenho de algoritmos de decisão para esta lógica revela dificuldades acrescidas.

Neste seminário, apresentaremos um cálculo de sequentes com etiquetas para a lógica proposicional bi-intuicionista e um algoritmo correcto e completo para a construção de provas neste cálculo, que, além da decisão das fórmulas da lógica, permite a extracção de contra-modelos de Kripke para os seus não-teoremas. (Trabalho conjunto com  Tarmo Uustalu.)
 
back 
 
  © 2024 Universidade do Minho  - Legal Terms  - updated by CMAT Símbolo de Acessibilidade na Web D.