Dissertação

Analytic classic-like tableaux for non-deterministic many-valued logics EVALUATED

Este trabalho tem como objectivo o desenvolvimento de um sistema de dedução para lógicas multivaloradas não-deterministas. Quando os recursos linguísticos da semântica são expressivos o suficiente, é possível usar a bivalência subjacente a estes sistemas para representar lógicas multivaloradas recorrendo apenas a dois valores lógicos. Deste modo a semântica original pode ser reduzida a uma semântica bivalente, e uma caracterização construtiva pode ser desenvolvida. Um sistema de dedução de tableaux pode ser extraído da semântica bivalente, juntamente com uma estratégia para garantir a terminação do método. Este sistema de um modo geral preserva algumas características da lógica clássica: as formulas presentes nas regras adotam exatamente os dois valores lógicos clássicos. Além disso, é provado que o sistema desenvolvido é correcto e completo, para além de satisfazer uma noção geral de analíticidade. Estes resultados são aplicáveis a outras classes de lógicas não-clássicas, como é o caso particular de lógicas com semânticas determinísticas multivaloradas, e o sistema de tableaux permite a dedução de contra-modelos em qualquer lógica multivalorada não-determinista. Por último esta tese debruça-se sobre a implementação de uma aplicação para geração automática do sistema de prova desenvolvido.
lógicas multivaloradas, não-determinismo, bivalência, tableaux, sistemas de dedução

Junho 29, 2018, 14:0

Publicação

Obra sujeita a Direitos de Autor

Orientação

ORIENTADOR

Carlos Manuel Costa Lourenço Caleiro

Departamento de Matemática (DM)

Professor Associado