Sequentes como duais dos tableaux para lógicas polivalentes

Abstract

A utilização de métodos dedutivos alternativos ao axiomático (hilbertiano) tem sido de grande interesse para a Teoria da Prova e para a Teoria da Computação, sendo esta última caracterizada pela busca por métodos mais adequados para implementações em computadores. Dentre tais métodos, abordaremos o cálculo de sequentes, proposto por Gentzen em 1935 e o método dos tableaux analíticos introduzido por Smullyan em 1968. Explicitamos uma sistematização a partir da proposta de Carnielli (1991) de como estabelecer sequentes como duais dos tableaux para lógicas polivalentes, promovendo um processo de dualização mais intuitivo a partir da formalização do tableau feita por Smullyan. Ademais, apresentaremos as regras em um sistema de sequentes para o cálculo proposicional clássico, a partir das regras de um sistema de tableaux, dualizando cada regra em tableau para um sequente adequado.