In *CEUR Workshop Proceedings*, volume 2585, pages 106-118, 2020.

Paper abstract bibtex

Paper abstract bibtex

We present a dual sequent calculus for the necessity fragment of the constructive modal logic S4 and show its adequacy for proof-search in the style of modern interactive theorem provers. The main feature of dual systems is the use of two contexts to capture the notions of true and valid formulas, without using any formal semantics. This attribute allows us to give simple rules for the □ operator that, most of the time, grant the substitution of a strict modal reasoning by a pure propositional one, thus simplifying the proof-search process. Moreover, we introduce a formal notion of backward proof corresponding to a bottom-up construction of a derivation tree by means of a left-to-right depth-first proof-search.

@inproceedings{ title = {On interactive proof-search for constructive modal necessity}, type = {inproceedings}, year = {2020}, identifiers = {[object Object]}, keywords = {Constructive Modal logic,Necessity,Proof-search,Sequent calculus}, pages = {106-118}, volume = {2585}, id = {4ba94759-7c1f-3a1f-b1b8-a1bdb01a8053}, created = {2020-11-25T00:57:34.194Z}, file_attached = {true}, profile_id = {b90fa0f0-b835-3487-8645-24bb43c8aba5}, group_id = {a91e2012-a2d1-3475-84d1-ff2f8b2ca743}, last_modified = {2020-11-25T01:01:45.791Z}, read = {false}, starred = {false}, authored = {false}, confirmed = {true}, hidden = {false}, citation_key = {Miranda-Perea2020}, folder_uuids = {cb689628-8825-4be3-9526-cd1da4d0adff}, private_publication = {false}, abstract = {We present a dual sequent calculus for the necessity fragment of the constructive modal logic S4 and show its adequacy for proof-search in the style of modern interactive theorem provers. The main feature of dual systems is the use of two contexts to capture the notions of true and valid formulas, without using any formal semantics. This attribute allows us to give simple rules for the □ operator that, most of the time, grant the substitution of a strict modal reasoning by a pure propositional one, thus simplifying the proof-search process. Moreover, we introduce a formal notion of backward proof corresponding to a bottom-up construction of a derivation tree by means of a left-to-right depth-first proof-search.}, bibtype = {inproceedings}, author = {Miranda-Perea, Favio E. and González Huesca, Lourdes del Carmen and Selene Linares-Arévalo, P.}, booktitle = {CEUR Workshop Proceedings} }

Downloads: 0