Tableaux for Łukasiewicz Infinite-valued Logic

被引：13
|
作者：
Nicola Olivetti
机构：
[1] Università di Torino,Diparimento di Informatica
来源：
Studia Logica | 2003年 / 73卷 / 1期
关键词：
many-valued logic; tableau methods; labelled proof systems; linear programming;
D O I：
10.1023/A:1022989323091
中图分类号：
学科分类号：
摘要：
In this work we propose a labelled tableau method for Łukasiewicz infinite-valued logic Lω. The method is based on the Kripke semantics of this logic developed by Urquhart [25] and Scott [24]. On the one hand, our method falls under the general paradigm of labelled deduction [8] and it is rather close to the tableau systems for sub-structural logics proposed in [4]. On the other hand, it provides a CoNP decision procedure for Lω validity by reducing the check of branch closure to linear programming
引用
收藏
页码：81 / 111
页数：30
相关论文
共 50 条
12345