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

DOI10.1016/S0304-3975(98)00012-7zbMATH Open0921.03013MaRDI QIDQ1276262FDOQ1276262

Authors: N. Olivetti, Daniele Mundici 

Publication date: 22 March 1999

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

Recommendations

• Computational complexity of infinite-valued Łukasiewicz propositional logic
• Satisfiability checking in Łukasiewicz logic as finite constraint satisfaction
• New complexity results for Łukasiewicz logic
• Probably partially true: satisfiability for Łukasiewicz infinitely-valued probabilistic logic and related topics
• scientific article; zbMATH DE number 549996

zbMATH Keywords

complexitymodel buildingdecision algorithmresolution procedureinfinite-valued calculus of Łukasiewicz

Mathematics Subject Classification ID

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

Cites Work

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

Cited In (15)

• Dual tableau for monoidal triangular norm logic MTL
• Computational complexity of infinite-valued Łukasiewicz propositional logic
• On the complexity of validity degrees in Łukasiewicz logic
• Graded many-valued resolution with aggregation.
• The complexity of McNaughton functions of one variable
• Satisfiability checking in Łukasiewicz logic as finite constraint satisfaction
• New complexity results for Łukasiewicz logic
• The complexity of 3-valued Łukasiewicz rules
• Automated theorem proving by resolution in non-classical logics
• Title not available (Why is that?)
• Giles's game and the proof theory of Łukasiewicz logic
• Determination of \(\alpha \)-resolution in lattice-valued first-order logic \(\mathrm{LF}(X)\)
• The MaxSAT problem in the real-valued MV-algebra
• Finite-valued reductions of infinite-valued logics
• On compatibilities of \(\alpha \)-lock resolution method in linguistic truth-valued lattice-valued logic

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1276262)