Interactive Matching Logic Proofs in Coq

Varování

Publikace nespadá pod Filozofickou fakultu, ale pod Fakultu informatiky. Oficiální stránka publikace je na webu muni.cz.
Autoři

TUŠIL Jan PÉTER Bereczky DÁNIEL Horpácsi

Rok publikování 2023
Druh Článek ve sborníku
Konference Theoretical Aspects of Computing (ICTAC 2023)
Fakulta / Pracoviště MU

Fakulta informatiky

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:

Používáte starou verzi internetového prohlížeče. Doporučujeme aktualizovat Váš prohlížeč na nejnovější verzi.