×

zbMATH — the first resource for mathematics

Resolution and model building in the infinite-valued calculus of Łukasiewicz. (English) Zbl 0921.03013
The paper presents a resolution procedure for the infinite-valued calculus of Łukasiewicz. Problems of resolution, model building and their complexity are discussed. The notion of \(\Theta\)-satisfiability is introduced. Then the authors prove that the \(\Theta\)-satisfiability problem is NP-complete. In the particular case of a finite set of Horn-clauses the authors provide decision and model building algorithms that are polynomial. The same is proved for a finite set of Krom-clauses.
Reviewer: N.Zamov (Kazan’)

MSC:
03B35 Mechanization of proofs and logical operations
03B50 Many-valued logic
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Imaz, G.Escalada; Serres, F.Manyiá, The satisfiability problem for multiple-valued Horn formulae, (), 250-256
[2] Hähnle, R., Exploiting data dependencies in many-valued logics, J. appl. non-classical logics, 6, 49-69, (1996) · Zbl 0836.03013
[3] Krom, M.R., The decision problem for formulas in prenex conjunctive normal form with binary disjunctions, J. symbolic logic, 35, 210-216, (1970) · Zbl 0207.01301
[4] \( L̵\)ukasiewicz, J.; Tarski, A., Untersuchungen über den aussagenkalkül, Comptes rendus Séances société sciences lettres varsovie, classe III, 23, 30-50, (1930), English translation in: [11, Ch. IV]. · JFM 57.1319.01
[5] McNaughton, R., A theorem about infinite-valued sentential logic, J. symbolic logic, 16, 1-13, (1951) · Zbl 0043.00901
[6] Mundici, D., Satisfiability in many-valued sentential logic is NP-complete, Theoret. comput. sci., 52, 145-153, (1987) · Zbl 0639.03042
[7] Mundici, D., Logic of infinite quantum systems, Internat. J. theoret. phys., 32, 1941-1955, (1993) · Zbl 0799.03019
[8] Mundici, D., \( L̵\)lukasiewicz normal forms and toric desingularizations, (), 401-423 · Zbl 0865.03014
[9] Mundici, D.; Trombetta, A., Optimal comparison strategies in Ulam’s searching game with errors, Theoret. comput. sci., 182, 217-232, (1997) · Zbl 0902.90191
[10] Rose, A.; Rosser, J.B., Fragments of many-valued statement calculi, Trans. amer. math. soc., 87, 1-53, (1958) · Zbl 0085.24303
[11] Tarski, A.; Tarski, A., Logic, semantics, metamathematics, (1983), Hackett Indianapolis, Reprinted · JFM 57.1318.03
[12] Vojtás̆, P.; Paulík, L., Soundness and completeness of non-classical extended SLD-resolution, (), 289-301
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.