On interactive proof-search for constructive modal necessity. Miranda-Perea, F., E.; González Huesca, L., d., C.; and Selene Linares-Arévalo, P. In CEUR Workshop Proceedings, volume 2585, pages 106-118, 2020.
On interactive proof-search for constructive modal necessity [pdf]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