Skip to main content
SpringerLink
Log in

Tableaux for Łukasiewicz Infinite-valued Logic

  • Published:
Studia Logica Aims and scope Submit manuscript

Abstract

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

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

References

  1. Aguzzoli, S., and A. Ciabattoni, ‘Finiteness in infinite-valued Łukasiewicz Logic’, Journal of Logic, Language and Information 9:5–29, 2000.

    Google Scholar 

  2. Avron, A., ‘Natural 3-valued Logics. Characterization and Proof Theory’, Journal of Symbolic Logic 56:276–294, 1991.

    Google Scholar 

  3. Ciabattoni, A., D. Gabbay, and N. Olivetti, ‘Cut-free proof systems for logics of weak excluded middle’, Soft Computing 2:147–156, 1999.

    Google Scholar 

  4. D'Agostino, M., and D. Gabbay, ‘A generalization of analytic deduction via labelled deductive systems I: basic substructural logics’, Journal of Automated Reasoning, 13:243–281, 1994.

    Google Scholar 

  5. D'Agostino, M., D. Gabbay, and K. Broda, ‘Tableau methods for substructural logics’, in: M. D'Agostino et al. (eds.): Handbook of Tableau Methods. Kluwer Academic Publishers, Dordrecht, pp. 469–528, 1999.

    Google Scholar 

  6. DoŠen, K., ‘Sequent systems and grupoid models II’, Studia Logica 48:41–65, 1989.

    Google Scholar 

  7. Fine, K., ‘Models for entailment’, Journal of Philosophical Logic 3: 347–372, 1974.

    Google Scholar 

  8. Gabbay, D., Labelled Deductive Systems (vol I), Oxford Logic Guides, Oxford University Press, 1996.

  9. Godo, L., and F. Esteva, ‘Monoidal T-norm based logic: Towards a logic for left-continuous T-norms’, Fuzzy-Sets and Systems: 124: 271–288, 2001.

    Google Scholar 

  10. HÄhnle, R., Automated Deduction in Multiple-valued logic. Oxford University Press, 1993.

  11. HÄhnle, R., ‘Many-valued logic and mixed-integer programming’, Annals of Mathematics and Artificial Intelligence 12: 231–264, 1994.

    Google Scholar 

  12. HÄhnle, R., ‘Tableaux for many-valued logics’, in: M. D'Agostino et al. (eds.): Handbook of Tableau Methods. Kluwer Academic Publishers, Dordrecht, pp. 529–580, 1999.

    Google Scholar 

  13. HÁjek, P., Metamathematics of Fuzzy Logic, Kluwer Academic Publishers, Dordrecht, 1998.

    Google Scholar 

  14. HÖhle, U., ‘Commutative, residuated l-monoids’, in: U. Höhle and P. Klement (eds.): Nonclassical logics and their applications to fuzzy subsets. Kluwer Academic Publishers, Dordrecht, pp. 53–106, 1995.

    Google Scholar 

  15. Jeroslow, G., Logic-Based Decision Support. Mixed Integer Model Formulation, Elsevier, Amsterdam, 1988.

    Google Scholar 

  16. Łukasiewicz, J., Tarski, A., ‘Untersuchungen über den Aussagenkalkül’, Comptes Rendus des séances de la Société des Sciences et des Lettres de Varsovie Classe III, 23:30–50, 1930.

    Google Scholar 

  17. Miglioli, P., U. Moscato, and M. Ornaghi, ‘An improved refutation system for intuitionistic predicate logic’, Journal of Automated Reasoning, 13(3): 361–374, 1994.

    Google Scholar 

  18. Mundici, D., ‘Satisfiability in many-valued sentential logic is NP-complete’, Theoretical Computer Science, 52:145–153, 1987.

    Google Scholar 

  19. Mundici, D., and N. Olivetti, ‘Resolution and model building in the infinite-valued calculus of Łukasiewicz’, Theoretical Computer Science, 200: 335–366, 1998.

    Google Scholar 

  20. Ono, H., and Y. Komori, ‘Logics without the contraction rule’, Journal of Symbolic Logic, 50: 169–201, 1985.

    Google Scholar 

  21. Ono, H., ‘Semantics for substructural logics’, in: P. Schroeder-Heister and K. Dosšen (eds.): Substructural Logics, pp. 259–291, Oxford University Press, 1993.

  22. Ono, H., ‘Logics without contraction rule and residuated lattices'. To appear in R. K. Meyer Festschrift, 2001.

  23. Prijatelj, A., ‘Bounded Contraction and Gentzen style Formulation of Łukasiewicz Logics’, Studia Logica, 57:437–456, 1996.

    Google Scholar 

  24. Scott, D., ‘Completeness and Axiomatizability in many-valued logic, in: Proc. of Tarski Symposium vol. XXV, AMS, pp. 411–435, 1974.

  25. Urquhart, A., ‘Many-Valued logic’, in: D. Gabbay and F. Guenther (eds): Handbook of Philosophical logic, Vol. 3, pp.71–116. D. Reidel, Dordrecht, 1986.

    Google Scholar 

  26. Wagner, H., ‘A new resolution calculus for the infinite-valued propositional logic of Łukasiewicz’, Journal of Applied Non-classical Logic. To appear, 2002.

Download references

Author information

Authors and Affiliations

  1. Diparimento di Informatica, Università di Torino, C.so Svizzera 185, 10149, Torino, Italy

    Nicola Olivetti

Authors
  1. Nicola Olivetti
    View author publications

    You can also search for this author in PubMed Google Scholar

Rights and permissions

Reprints and permissions

About this article

Cite this article

Olivetti, N. Tableaux for Łukasiewicz Infinite-valued Logic. Studia Logica 73, 81–111 (2003). https://doi.org/10.1023/A:1022989323091

Download citation

  • Issue Date:

  • DOI: https://doi.org/10.1023/A:1022989323091

Search

Navigation