In this paper we define internal cut-free sequent calculi for any n-valued Lukasiewicz logic Ln. These calculi are based on a representation of formulas of Ln, by n - 1 many {0, 1}-valued formulas of Ln. They enjoy the usual properties of sequent systems like symmetry, subformula property and invertibility of the rules. Upon dualizing our calculi one obtains Hähnle's tableau systems. Then they provide a reformulation of Hähnle's approach to theorem proving that makes no use of nonlogical elements.
Sequent calculi for finite-valued Lukasiewicz logics via Boolean decompositions / S. Aguzzoli, A. Ciabattoni, A. Di Nola. - In: JOURNAL OF LOGIC AND COMPUTATION. - ISSN 0955-792X. - 10:2(2000 Apr), pp. 213-222. [10.1093/logcom/10.2.213]
Sequent calculi for finite-valued Lukasiewicz logics via Boolean decompositions
S. AguzzoliPrimo
;
2000
Abstract
In this paper we define internal cut-free sequent calculi for any n-valued Lukasiewicz logic Ln. These calculi are based on a representation of formulas of Ln, by n - 1 many {0, 1}-valued formulas of Ln. They enjoy the usual properties of sequent systems like symmetry, subformula property and invertibility of the rules. Upon dualizing our calculi one obtains Hähnle's tableau systems. Then they provide a reformulation of Hähnle's approach to theorem proving that makes no use of nonlogical elements.
Pubblicazioni consigliate
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
