Resolution and model building in the infinite-valued calculus of Łukasiewicz

DOI10.1016/S0304-3975(98)00012-7zbMath0921.03013MaRDI QIDQ1276262

Nicola Olivetti, Daniele Mundici

Publication date: 22 March 1999

Published in: Theoretical Computer Science (Search for Journal in Brave)

zbMATH Keywords

complexitymodel buildingdecision algorithminfinite-valued calculus of Łukasiewiczresolution procedure

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Many-valued logic (03B50)

Related Items (10)

Automated theorem proving by resolution in non-classical logics ⋮ Satisfiability checking in Łukasiewicz logic as finite constraint satisfaction ⋮ On compatibilities of \(\alpha \)-lock resolution method in linguistic truth-valued lattice-valued logic ⋮ Dual tableau for monoidal triangular norm logic MTL ⋮ Graded many-valued resolution with aggregation. ⋮ Determination of \(\alpha \)-resolution in lattice-valued first-order logic \(\mathrm{LF}(X)\) ⋮ The complexity of McNaughton functions of one variable ⋮ New complexity results for Łukasiewicz logic ⋮ Giles's game and the proof theory of Łukasiewicz logic ⋮ On the complexity of validity degrees in Łukasiewicz logic

Cites Work

• Unnamed Item
• Satisfiability in many-valued sentential logic is NP-complete
• Logic of infinite quantum systems
• Optimal comparison strategies in Ulam's searching game with two errors
• Fragments of Many-Valued Statement Calculi
• Exploiting data dependencies in many-valued logics
• The decision problem for formulas in prenex conjunctive normal form with binary disjunctions
• A theorem about infinite-valued sentential logic

This page was built for publication: Resolution and model building in the infinite-valued calculus of Łukasiewicz