Abstract :
A t-norm logic L* is the logic of a standard algebra [0, 1]* = ([0, 1], *, →*, 0), for * being a continuous t-norm and →* its residuum. The notion of canonical t-algebra introduced by Hanikova (Neural Network World, vol.12, p.453-460, 2002) and Esteva-Godo-Montagna (Equational characterization of the subvarieties of BL generated by t-norm algebras), the sets-as-signs approach to many-valued tableau systems by Hahnle (Automated Deduction in Multiple-Valued Logics, Oxford University Press, Oxford, 1994), and finite-valued reduction techniques (S. Aguzzoli et al., Journal of Logic, Language and Information, vol.9, p.5-29, 2000; and S. Aguzzoli et al., Archive for Mathematical Logic, vol.41, p.361-399, 2002) allow us to describe in a uniform way co-NP calculi for all t-norm logics.
Keywords :
algebra; calculus; formal logic; theorem proving; binary operations; canonical t-algebra; co-NP calculi; continuous t-norm residuum; finite-valued reduction techniques; proof trees; sets-as-signs many-valued tableau systems; standard algebra logic; t-norm logic calculi; AC generators; Algebra; Fuzzy logic; Lattices; Logic functions; Multivalued logic;
