A New Method to Obtain Termination in Backward Proof Search For Modal Logic S4

DOI10.1093/logcom/exn071zbMath1189.03020OpenAlexW1967844876MaRDI QIDQ3406694

A. Ju. Pljuskevicene, Regimantas Pliuškevičius

Publication date: 19 February 2010

Published in: Journal of Logic and Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1093/logcom/exn071

zbMATH Keywords

modal logicsequent calculusterminationdecision procedurebackward proof searchloop check

Mathematics Subject Classification ID

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

Related Items (4)

Logical derivation search with assumption traceability ⋮ A dual-context sequent calculus for the constructive modal logic S4 ⋮ On interactive proof-search for constructive modal necessity ⋮ Loop-free calculus for modal logic S4. I

This page was built for publication: A New Method to Obtain Termination in Backward Proof Search For Modal Logic S4