Zde se nacházíte:
Informace o publikaci
Interactive Matching Logic Proofs in Coq
Autoři | |
---|---|
Rok publikování | 2023 |
Druh | Článek ve sborníku |
Konference | Theoretical Aspects of Computing (ICTAC 2023) |
Fakulta / Pracoviště MU | |
Citace | |
Doi | http://dx.doi.org/10.1007/978-3-031-47963-2_10 |
Klíčová slova | Matching logic; Sequent calculus; Coq; Interactive reasoning |
Přiložené soubory | |
Popis | Matching logika (ML) je formalismus pro specifikaci a uvažování o matematických strukturách pomocí vzorů a jejich shody. V minulosti byla tato logika použita k popisu jiných logik, například separační logiky s rekurzivními definicemi a lineární temporální logiky. ML byla také formalizována v důkazovém asistentu Coq, v němž byl i mechanizován důkaz korektnosti Hilbertovského odvozovacího systému ML. Nicméně, používat Hilbertovský odvozovací systém pro interaktivní uvažování je náročné - tím spíše v ML, ve které neplatí obecná věta o dedukci. Proto nabízíme jednozávěrový sekvent kalkulus pro ML, jež je vhodnější k interaktivnímu dokazování. Na tomto sekvent kalkulu implementujeme důkazový režim pro interaktivní uvažování v ML, který významným způsobem zjednodušuje konstrukci ML důkazů v Coqu. Tento důkazový režim je mechanismus pro zobrazování mezi-stavů důkazů spolu s rozšiřitelnou sadou dokazovacích taktik implementujících pravidla našeho sekvent kalkulu. Důkazový režim vyhodnocujeme na sadě příkladů, čímž ilustrujeme významné zlepšení ve velikosti důkazových skriptů a čitelnosti. |
Související projekty: |