The resolution method for one reducible class of formulas of the first-order modal logic S4.

DOI10.1007/S10986-005-0016-5MaRDI QIDQ2487862zbMATH OpenOpenAlexFDO

Authors Yanyan Li

Publication date 9 August 2005

Published in Lithuanian Mathematical Journal (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s10986-005-0016-5

zbMATH Keywords

absorption tacticsmodal logic S4proof searchresolution method

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Modal logic (including the logic of norms) (03B45)

Recommendations

• scientific article; zbMATH DE number 4128785
• scientific article; zbMATH DE number 1880278
• Modal resolution in clausal form
• Resolution for some first-order modal systems
• scientific article; zbMATH DE number 3902618

Cites work

• Herbrand style proof procedures for modal logic
• scientific article; zbMATH DE number 510785 (Why is no real title available?)
• scientific article; zbMATH DE number 3441640 (Why is no real title available?)
• scientific article; zbMATH DE number 1418446 (Why is no real title available?)
• Resolution for some first-order modal systems

Cited in

(3)

• scientific article; zbMATH DE number 3902618 (Why is no real title available?)
• scientific article; zbMATH DE number 4128785 (Why is no real title available?)
• scientific article; zbMATH DE number 1880278 (Why is no real title available?)

This page was built for publication: The resolution method for one reducible class of formulas of the first-order modal logic S4.

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