More Web Proxy on the site http://driver.im/

article

Sequent and hypersequent calculi for abelian and łukasiewicz logics

Authors:

George Metcalfe,

Nicola Olivetti,

Dov GabbayAuthors Info & Claims

ACM Transactions on Computational Logic (TOCL), Volume 6, Issue 3

Pages 578 - 613

https://doi.org/10.1145/1071596.1071600

Published: 01 July 2005 Publication History

Abstract

We present two embeddings of Łukasiewicz logic Ł into Meyer and Slaney's Abelian logic A, the logic of lattice-ordered Abelian groups. We give new analytic proof systems for A and use the embeddings to derive corresponding systems for Ł. These include hypersequent calculi, terminating hypersequent calculi, co-NP labeled sequent calculi, and unlabeled sequent calculi.

References

[1]

Aguzzoli, S. and Ciabattoni, A. 2000. Finiteness in infinite-valued logic. J. Logic, Lang. Inform. 9, 1, 5--29.]]

[2]

Aguzzoli, S. and Gerla, B. 2002. Finite-valued reductions of infinite-valued logics. Arch. Math. Logic 41, 4, 361--399.]]

[3]

Anderson, A. R. and Belnap, N. D. 1975. Entailment. Vol. 1. Princeton University Press, Princeton, NJ.]]

[4]

Avron, A. 1987. A constructive analysis of RM. J. Symbol. Logic 52, 4, 939--951.]]

[5]

Avron, A. 1991. Hypersequents, logical consequence and intermediate logics for concurrency. Ann. Math. Art. Intell. 4, 3--4, 225--248.]]

[6]

Avron, A. 1996. The method of hypersequents in the proof theory of propositional non-classical logics. In Logic: From Foundations to Applications. Proceedings of the Logic Colloquium, Keele, UK, 1993, W. Hodges, M. Hyland, C. Steinhorn, and J. Truss, Eds. Oxford University Press, New York, NY, 1--32.]]

[7]

Avron, A. and Konikowska, B. 2001. Decomposition proof systems for Gödel-Dummett logics. Studia Logica 69, 2, 197--219.]]

[8]

Baaz, M., Ciabattoni, A., and Montagna, F. 2004. Analytic calculi for monoidal t-norm based logic. Fundamenta Informaticae. 59, 4, 315--332.]]

[9]

Baaz, M. and Fermüller, C. G. 1999. Analytic calculi for projective logics. In Proceedings of TABLEAUX '99. Vol. 1617. 36--50.]]

[10]

Casari, E. 1989. Comparative logics and Abelian l-groups. In Logic Colloquium '88, C. Bonotto, R. Ferro, S. Valentini, and A. Zanardo, Eds. Elsevier, Amsterdam, The Netherlands, 161--190.]]

[11]

Chang, C. C. 1958. Algebraic analysis of many-valued logics. Trans. Amer. Math. Soc. 88, 467--490.]]

[12]

Ciabattoni, A., Esteva, F., and Godo, L. 2002. T-norm based logics with n-contraction. Neural Netw. World 12, 5, 441--453.]]

[13]

Ciabattoni, A. and Metcalfe, G. 2003. Bounded Łukasiewicz logics. In Proceedings of TABLEAUX 2003, M. C. Mayer and F. Pirri, Eds. Lecture Notes in Computer Science, vol. 2796. Springer, Berlin, Germany.]]

[14]

Cignoli, R., D'Ottaviano, I. M. L., and Mundici, D. 1999. Algebraic Foundations of Many-Valued Reasoning. Trends in Logic, vol. 7. Kluwer, Dordrecht, The Netherlands.]]

[15]

Cignoli, R., Esteva, F., Godo, L., and Torrens, A. 2000. Basic fuzzy logic is the logic of continuous t-norms and their residua. Soft Comput. 4, 2, 106--112.]]

[16]

Dunn, J. M. and Meyer, R. K. 1971. Algebraic completeness results for Dummett's LC and its extensions. Zeitsch. Math. Logik Grund. Mathemat. 17, 225--230.]]

[17]

Dyckhoff, R. 1999. A deterministic terminating sequent calculus for Gödel-Dummett logic. Logic J. IGPL 7, 3, 319--326.]]

[18]

Esteva, F., Gispert, J., Godo, L., and Montagna, F. 2002. On the standard and rational completeness of some axiomatic extensions of the monoidal t-norm logic. Studia Logica 71, 2, 199--226.]]

[19]

Esteva, F. and Godo, L. 2001. Monoidal t-norm based logic: Towards a logic for left-continuous t-norms. Fuzzy Sets Syst. 124, 271--288.]]

[20]

Galli, A., Lewin, R. A., and Sagastume, M. 2004. The logic of equilibrium and Abelian lattice ordered groups. Arch. Math. Logic 43, 2, 141--158.]]

[21]

Gottwald, S. 2000. A Treatise on Many-Valued Logics. Studies in Logic and Computation, vol. 9. Research Studies Press, Baldock, Herts., U.K.]]

[22]

Gurevich, Y. S. and Kokorin, A. I. 1963. Universal equivalence of ordered Abelian groups (in Russian). Algebra i logika 2, 37--39.]]

[23]

Hähnle, R. 1993. Automated Deduction in Multiple-Valued Logics. Oxford University Press, Oxford, U.K.]]

[24]

Hájek, P. 1998. Metamathematics of Fuzzy Logic. Kluwer Academic Publishers, Dordrecht, The Netherlands.]]

[25]

Höhle, U. 1995. Commutative, residuated &ell;-monoids. In Non-Classical Logics and their Applications to Fuzzy Subsets, U. Höhle and E. P. Klement, Eds. Kluwer, Dordrecht, The Netherlands, 53--106.]]

[26]

Jenei, S. and Montagna, F. 2002. A proof of standard completeness for Esteva and Godo's MTL logic. Studia Logica 70, 2, 183--192.]]

[27]

Klement, E. P., Mesiar, R., and Pap, E. 2000. Triangular Norms. Trends in Logic, vol. 8. Kluwer, Dordrecht, The Netherlands.]]

[28]

Łukasiewicz, J. 1970. Jan Łukasiewicz, Selected Writings, L. Borowski, Ed. North Holland, The Netherlands.]]

[29]

Łukasiewicz, J. and Tarski, A. 1930. Untersuchungen über den Aussagenkalkül. Comptes Ren- dus des Séances de la Societé des Sciences et des Lettres de Varsovie, Classe III 23. Reprinted and translated in Łukasiewicz {1970}.]]

[30]

Malinowski, G. 1993. Many-Valued Logics. Oxford Logic Guides, vol. 25. Oxford University Press, Oxford, U.K.]]

[31]

Metcalfe, G., Olivetti, N., and Gabbay, D. 2002. Analytic sequent calculi for Abelian and Łukasiewicz logics. In Proceedings of TABLEAUX 2002, U. Egly and C. G. Fermüller, Eds. Lecture Notes in Computer Science, vol. 2381. Springer, Berlin, Germany, 191--205.]]

[32]

Metcalfe, G., Olivetti, N., and Gabbay, D. 2004. Analytic proof calculi for product logics. Arch. Math. Logic 43, 7, 859--889.]]

[33]

Meyer, R. K. 1973. Intuitionism, entailment, negation. In Truth, Syntax and Modality, H. Leblanc, Ed. North Holland, Amsterdam, The Netherlands, 168--198.]]

[34]

Meyer, R. K. and Slaney, J. K. 1989. Abelian logic from A to Z. In Paraconsistent Logic: Essays on the Inconsistent, G. Priest, R. Sylvan, and J. Norman, Eds. Philosophia Verlag, Munich, Germany, 245--288.]]

[35]

Montagna, F., Pinna, G. M., and Tiezzi, E. B. P. 2003. A tableau calculus for Hájek's logic BL. J. Logic Computat. 13, 2, 241--259.]]

[36]

Mundici, D. 1987. Satisfiability in many-valued sentential logic is NP-complete. Theoret. Comput. Sci. 52, 12, 145--153.]]

[37]

Mundici, D. and Olivetti, N. 1998. Resolution and model building in the infinite-valued calculus of Łukasiewicz. Theoret. Comput. Sci. 200, 1--2, 335--366.]]

[38]

Olivetti, N. 2003. Tableaux for Łukasiewicz infinite-valued logic. Studia Logica 73, 1, 81--111.]]

[39]

Paoli, F. 2001. Logic and groups. Logic Logical Philos. 9, 109--128.]]

[40]

Pottinger, G. 1983. Uniform, cut-free formulations of T, S4 and S5 (abstract). J. Symbol. Logic 48, 3, 900.]]

[41]

Prijatelj, A. 1996. Bounded contraction and Gentzen-style formulation of Łukasiewicz logics. Studia Logica 57, 2--3, 437--456.]]

[42]

Rose, A. and Rosser, J. B. 1958. Fragments of many-valued statement calculi. Trans. Amer. Math. Soc. 87, 1--53.]]

[43]

Schrijver, A. 1987. Theory of Linear and Integer Programming. John Wiley and Sons, New York, NY.]]

[44]

Scott, D. 1974. Completeness and axiomatizability in many-valued logic. In Proceedings of Symposia in Pure Mathematics Volume XXV: Proceedings of the Tarski Symposium, L. Henkin et al., Eds. American Mathematical Society, Berkeley, CA, 411--435.]]

[45]

Urquhart, A. 1986. Many-valued logics. In Handbook of Philosophical Logic, vol. 3. D. Gabbay and F. Günthner, Eds. Reidel, Dordrecht, The Netherlands, 71--116.]]

[46]

Weispfenning, V. 1986. The complexity of the word problem for Abelian l-groups. Theoret. Comput. Sci. 48, 1, 127--132.]]

Cited By

Mohammadi H(2023)Linear Abelian Modal LogicBulletin of the Section of Logic10.18778/0138-0680.2023.3053:1(1-28)Online publication date: 15-Dec-2023
https://doi.org/10.18778/0138-0680.2023.30
BADIA GBĚHOUNEK LCINTULA PTEDDER A(2023)RELEVANT CONSEQUENCE RELATIONS: AN INVITATIONThe Review of Symbolic Logic10.1017/S1755020323000205(1-31)Online publication date: 30-Jun-2023
https://doi.org/10.1017/S1755020323000205
Niki SWansing H(2023)On the Provable Contradictions of the Connexive Logics C and C3Journal of Philosophical Logic10.1007/s10992-023-09709-4Online publication date: 29-Jul-2023
https://doi.org/10.1007/s10992-023-09709-4
Show More Cited By

Index Terms

Sequent and hypersequent calculi for abelian and łukasiewicz logics
1. Computing methodologies
  1. Symbolic and algebraic manipulation
    1. Symbolic and algebraic algorithms
      1. Theorem proving algorithms
2. Theory of computation
  1. Logic
    1. Proof theory

Recommendations

Sequent calculi for propositional nonmonotonic logics

A uniform proof-theoretic reconstruction of the major nonmonotonic logics is introduced. It consists of analytic sequent calculi where the details of nonmonotonic assumption making are modelled by an axiomatic rejection method. Another distinctive ...
Proof Theory for Casari's Comparative Logics

Comparative logics were introduced by Casari in the 1980s to treat aspects of comparative reasoning occurring in natural language. In this article Gentzen systems are defined for these logics by means of a special mix rule that combines calculi for ...
Hypersequent Calculi for Modal Logics Extending S4
New Frontiers in Artificial Intelligence
Abstract
In this paper, we introduce hypersequent calculi for some modal logics extending S4 modal logic. In particular, we uniformly characterize hypersequent calculi for S4, S4.2, S4.3, S5 in terms of what are called “external modal structural rules” for ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Transactions on Computational Logic

ACM Transactions on Computational Logic Volume 6, Issue 3

July 2005

191 pages

ISSN:1529-3785

EISSN:1557-945X

DOI:10.1145/1071596

Issue’s Table of Contents

Copyright © 2005 ACM.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 July 2005

Published in TOCL Volume 6, Issue 3

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

39
Total Citations
View Citations
410
Total Downloads

Downloads (Last 12 months)9
Downloads (Last 6 weeks)2

Reflects downloads up to 11 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Mohammadi H(2023)Linear Abelian Modal LogicBulletin of the Section of Logic10.18778/0138-0680.2023.3053:1(1-28)Online publication date: 15-Dec-2023
https://doi.org/10.18778/0138-0680.2023.30
BADIA GBĚHOUNEK LCINTULA PTEDDER A(2023)RELEVANT CONSEQUENCE RELATIONS: AN INVITATIONThe Review of Symbolic Logic10.1017/S1755020323000205(1-31)Online publication date: 30-Jun-2023
https://doi.org/10.1017/S1755020323000205
Niki SWansing H(2023)On the Provable Contradictions of the Connexive Logics C and C3Journal of Philosophical Logic10.1007/s10992-023-09709-4Online publication date: 29-Jul-2023
https://doi.org/10.1007/s10992-023-09709-4
CAMPERCHOLI MCASTAÑO DDÍAZ VARELA JGISPERT J(2022)ALGEBRAIC EXPANSIONS OF LOGICSThe Journal of Symbolic Logic10.1017/jsl.2022.47(1-19)Online publication date: 22-Jun-2022
https://doi.org/10.1017/jsl.2022.47
Fermüller CLang TPavlova A(2022)From Truth Degree Comparison Games to Sequents-of-Relations Calculi for Gödel LogicLogica Universalis10.1007/s11787-022-00300-016:1-2(221-235)Online publication date: 7-Mar-2022
https://doi.org/10.1007/s11787-022-00300-0
Colacito AGalatos NMetcalfe G(2021)Theorems of Alternatives for Substructural LogicsArnon Avron on Semantics and Proof Theory of Non-Classical Logics10.1007/978-3-030-71258-7_5(91-105)Online publication date: 31-Jul-2021
https://doi.org/10.1007/978-3-030-71258-7_5
Niki SSchuster P(2020)On Scott’s semantics for many-valued logicJournal of Logic and Computation10.1093/logcom/exaa036Online publication date: 21-Jul-2020
https://doi.org/10.1093/logcom/exaa036
(2020)ConferencesLogic Journal of the IGPL10.1093/jigpal/jzaa004Online publication date: 12-Jun-2020
https://doi.org/10.1093/jigpal/jzaa004
Fermüller CLang TPavlova A(2020)From Truth Degree Comparison Games to Sequents-of-Relations Calculi for Gödel LogicInformation Processing and Management of Uncertainty in Knowledge-Based Systems10.1007/978-3-030-50146-4_20(257-270)Online publication date: 5-Jun-2020
https://doi.org/10.1007/978-3-030-50146-4_20
Lucas CMio M(2019)Towards a Structural Proof Theory of Probabilistic -CalculiFoundations of Software Science and Computation Structures10.1007/978-3-030-17127-8_24(418-435)Online publication date: 8-Apr-2019
https://dl.acm.org/doi/10.1007/978-3-030-17127-8_24
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Issue’s Table of Contents