@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}
}

{"_id":"S8rLfWEnNLKa2hbEY","bibbaseid":"mirandaperea-gonzlezhuesca-selenelinaresarvalo-oninteractiveproofsearchforconstructivemodalnecessity-2020","authorIDs":[],"author_short":["Miranda-Perea, F., E.","González Huesca, L., d., C.","Selene Linares-Arévalo, P."],"bibdata":{"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","bibtex":"@inproceedings{\n title = {On interactive proof-search for constructive modal necessity},\n type = {inproceedings},\n year = {2020},\n identifiers = {[object Object]},\n keywords = {Constructive Modal logic,Necessity,Proof-search,Sequent calculus},\n pages = {106-118},\n volume = {2585},\n id = {4ba94759-7c1f-3a1f-b1b8-a1bdb01a8053},\n created = {2020-11-25T00:57:34.194Z},\n file_attached = {true},\n profile_id = {b90fa0f0-b835-3487-8645-24bb43c8aba5},\n group_id = {a91e2012-a2d1-3475-84d1-ff2f8b2ca743},\n last_modified = {2020-11-25T01:01:45.791Z},\n read = {false},\n starred = {false},\n authored = {false},\n confirmed = {true},\n hidden = {false},\n citation_key = {Miranda-Perea2020},\n folder_uuids = {cb689628-8825-4be3-9526-cd1da4d0adff},\n private_publication = {false},\n 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.},\n bibtype = {inproceedings},\n author = {Miranda-Perea, Favio E. and González Huesca, Lourdes del Carmen and Selene Linares-Arévalo, P.},\n booktitle = {CEUR Workshop Proceedings}\n}","author_short":["Miranda-Perea, F., E.","González Huesca, L., d., C.","Selene Linares-Arévalo, P."],"urls":{"Paper":"https://bibbase.org/service/mendeley/b90fa0f0-b835-3487-8645-24bb43c8aba5/file/3d1e8d95-32a2-7c5b-268e-275ac90c4e96/2020_MirandaGonzálesLinares__OnInteractiveProof_search.pdf.pdf"},"bibbaseid":"mirandaperea-gonzlezhuesca-selenelinaresarvalo-oninteractiveproofsearchforconstructivemodalnecessity-2020","role":"author","keyword":["Constructive Modal logic","Necessity","Proof-search","Sequent calculus"],"downloads":0},"bibtype":"inproceedings","creationDate":"2020-11-26T03:10:30.175Z","downloads":0,"keywords":["constructive modal logic","necessity","proof-search","sequent calculus"],"search_terms":["interactive","proof","search","constructive","modal","necessity","miranda-perea","gonzález huesca","selene linares-arévalo"],"title":"On interactive proof-search for constructive modal necessity","year":2020}