Abstract
This paper is concerned with decision proceedures for the ℵ0-valued Łukasiewicz logics,
. It is shown how linear algebra can be used to construct an automated theorem checker. Two decision proceedures are described which depend on a linear programming package. An algorithm is given for the verification of consequence relations in
, and a connection is made between theorem checking in two-valued logic and theorem checking in
which implies that determing of a ⊃-free formula whether it takes the value one is NP-complete problem.
This is a preview of subscription content, log in via an institution to check access.
Similar content being viewed by others
References
Robert McNaughton,A theorem about infinite-valued sentential logic,The Journal of Symbolic Logic 16 (1951), pp. 1–13.
Daniele Mundici,Satisfiability in many-valued sentential logic is NP-complete,Theoretical Computer Science 52 (1987), pp. 145–153.
Alan Rose andJ. Barkley Rosser,Fragments of many-valued statement calculi,Transactions of the American Mathematical Society, vol. 87 (1958), pp. 1–53.
Author information
Authors and Affiliations
Rights and permissions
About this article
Cite this article
Beavers, G. Automated theorem proving for Łukasiewicz logics. Stud Logica 52, 183–195 (1993). https://doi.org/10.1007/BF01058388
Received:
Issue Date:
DOI: https://doi.org/10.1007/BF01058388