Proof theory for locally finite many-valued logics: semi-projective logics.

*(English)*Zbl 1322.03019As the authors explain, the aim of the article is to extend the methodology in [M. Baaz and C. G. Fermüller, Lect. Notes Comput. Sci. 1617, 36–50 (1999; Zbl 0931.03066)] to systematically construct analytic calculi for semi-projective logics – a large family of (propositional) locally finite many-valued logics. Such calculi, defined in the framework of sequents of relations, are proof search oriented and can be used to settle the computational complexity of the formalized logics. As a case study they derive sequent calculi of relations for nilpotent minimum logic (see [F. Esteva and L. Godo, Fuzzy Sets Syst. 124, No. 3, 271–288 (2001; Zbl 0994.03017)]) and for a family of axiomatic extensions of Hájek’s basic logic BL extended with the \(n\)-contraction axiom, (see [M. Bianchi and F. Montagna, Arch. Math. Logic 50, No. 3–4, 257–285 (2011; Zbl 1266.03041)]). The introduced calculi are used to prove that the decidability problem in these logics is Co-NP complete.

The main results are in Sections 3 to 5. Section 3 is about semi-projective logics, and presents a general method to construct an analytic calculi, for them. It is shown, among the other things, that every semi-projective logic with finitely-many connectives and constants is locally finite, and that all semi-projective logics are decidable. These results are then applied in Section 4, to present an analytic calculi for NM and for a family of \(n\)-contractive axiomatic extensions of BL. Moreover, it is also shown that such calculi provide a Co-NP decision procedure for the validity problem of these logics. Finally, in Section 5 is discussed the problem of defining analytic calculi for first-order many-valued logics, and most of the results are negative.

The main results are in Sections 3 to 5. Section 3 is about semi-projective logics, and presents a general method to construct an analytic calculi, for them. It is shown, among the other things, that every semi-projective logic with finitely-many connectives and constants is locally finite, and that all semi-projective logics are decidable. These results are then applied in Section 4, to present an analytic calculi for NM and for a family of \(n\)-contractive axiomatic extensions of BL. Moreover, it is also shown that such calculi provide a Co-NP decision procedure for the validity problem of these logics. Finally, in Section 5 is discussed the problem of defining analytic calculi for first-order many-valued logics, and most of the results are negative.

Reviewer: Matteo Bianchi (Milano)

##### MSC:

03B50 | Many-valued logic |

03F03 | Proof theory in general (including proof-theoretic semantics) |

03B25 | Decidability of theories and sets of sentences |

##### Keywords:

many-valued logic; analytic calculi; sequents of relations; nilpotent minimum logic; basic logic; first-order logics; computational complexity##### Software:

MUltlog
PDF
BibTeX
XML
Cite

\textit{A. Ciabattoni} and \textit{F. Montagna}, Theor. Comput. Sci. 480, 26--42 (2013; Zbl 1322.03019)

Full Text:
DOI

##### References:

[1] | S. Aguzzoli, B. Gerla, Comparing the expressive power of some fuzzy logics based on residuated \(t\)-norms, in: Proceedings of FUZZ-IEEE 2006, pp. 2012-2019. |

[2] | Avron, A., The method of hypersequents in the proof theory of propositional nonclassical logics, (Hodges, W.; Hyland, M.; Steinhorn, C.; Truss, J., Logic: From Foundations to Applications, European Logic Colloquium, (1996), Oxford Science Publications. Clarendon Press), 1-32 · Zbl 0861.03043 |

[3] | Bachmair, L.; Ganzinger, H., Ordered chaining calculi for first-order theories of transitive relations, Journal of the ACM, 45, 6, 1007-1049, (1998) · Zbl 1065.68615 |

[4] | Baaz, M.; Ciabattoni, A.; Fermüller, C., Cut-elimination in a sequents-of-relations calculus for Gödel logic, (Proceedings of ISMVL 2001, (2001), IEEE), 181-186 |

[5] | Baaz, M.; Fermüller, C., Analytic calculi for projective logics, (Proceedings of Automated Reasoning with Tableaux and Related Methods (Tableaux’99), LNAI, vol. 1617, (1999)), 36-51 · Zbl 0931.03066 |

[6] | Baaz, M.; Fermüller, C.; Salzer, G., Automated deduction for many-valued logics, Handbook of Automated Reasoning, 1355-1402, (2001) · Zbl 0992.03015 |

[7] | Baaz, M.; Fermüller, C.; Salzer, G.; Zach, R., Multlog 1.0: towards an expert system for many-valued logics, (Proceedings of CADE 1996, LNCS, vol. 1104, (1996)), 226-230 |

[8] | Bianchi, M.; Montagna, F., \(n\)-contractive BL-logics, Archive for Mathematical Logic, 50, 3-4, 257-285, (2011) · Zbl 1266.03041 |

[9] | Blok, W.; Pigozzi, D., Algebraizable logics, (Memoirs of the AMS, (1989), American Mathematical Society) · Zbl 0664.03042 |

[10] | Burris, S.; Sankappanavar, H. P., A course in universal algebra, (Graduate texts in Mathematics, (1981), Springer Verlag) · Zbl 0478.08001 |

[11] | Busaniche, M.; Cabrer, L., Canonicity in subvarieties of BL-algebras, Algebra Universalis, 62, 4, 375-397, (2009) · Zbl 1200.03049 |

[12] | Ciabattoni, A.; Fermüller, C.; Metcalfe, G., Uniform rules and dialogue games for fuzzy logics, (Proceedings of LPAR 2004, LNAI, vol. 3452, (2004)), 496-510 · Zbl 1109.03019 |

[13] | Cignoli, R.; D’Ottaviano, I. M. L.; Mundici, D., Algebraic foundations of many-valued reasoning, (1999), Kluwer Acad. Publ. Dordrecht · Zbl 0937.06009 |

[14] | Esteva, F.; Godo, L., Monoidal \(t\)-norm based logic: towards a logic for left-continuous \(t\)-norms, Fuzzy Sets and Systems, 3, 271-288, (2001) · Zbl 0994.03017 |

[15] | Esteva, F.; Godo, L.; Hájek, P.; Navara, M., Residuated fuzzy logics with an involutive negation, Archive for Mathematical Logic, 39, 2, 103-124, (2000) · Zbl 0965.03035 |

[16] | Flaminio, T.; Marchioni, E., \(T\)-norm-based logics with an independent involutive negation, Fuzzy Sets and Systems, 157, 24, 3125-3144, (2006) · Zbl 1114.03015 |

[17] | Hájek, P., Metamathematics of fuzzy logic, (1998), Kluwer Acad. Publ. Dordrecht · Zbl 0937.03030 |

[18] | Hájek, P.; Cintula, P., On theories and models in fuzzy predicate logics, Journal of Symbolic Logic, 71, 3, 863-880, (2006) · Zbl 1111.03030 |

[19] | Metcalfe, G.; Olivetti, N.; Gabbay, D., (Proof Theory for Fuzzy Logics, Springer Series in Applied Logic, vol. 36, (2008)) |

[20] | Vetterlein, T., Analytic calculi for logics of ordinal multiples of standard \(t\)-norms, Journal of Logic and Computation, 18, 1, 35-57, (2008) · Zbl 1139.03018 |

This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.