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: |