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