Automatizuotos taktikos Coq aplinkoje

Ištrauka

Automatizuotos taktikos Coq aplinkoje
Baigiamasis bakalauro darbas

Turinys
Įvadas 3
1. Automatizuota teoremų įrodymo aplinka Coq 5
1.1 Intuicionistinė logika Coq‘e 5
1.2 „Forward“ ir „backward“ proof 7
1.3 Coq loginė bazė 8
1.4 Coq taktikos 9
1.5 Teoremos įrodymo pavyzdys Coq‘e 14
2. Naujų taktikų kūrimas Coq‘e 16
2.1 Ltac kalba 16
2.2 Paprastų teiginių logikos uždavinių automatizavimas 21
2.3 Uždavinių, besiremiančių induktyviai apibrėžtais teiginiais, automatizavimas 32
2.4 Deklaratyvi kalba 51
2.5 Deklaratyvaus stiliaus taktikų kūrimas Coq aplinkoje 52
Darbo rezultatai 61
Išvados 62
Summary 64
Literatūros sąrašas 65

Įvadas
Šiame bakalauro baigiamajame darbe, naudojantis teoremų įrodymo aplinka Coq [BC04],
yra tiriami automatizuoto verifikavimo metodų išplėtimo ir įrodymų skaitomumo gerinimo būdai.
Coq yra interaktyvi pagalbinė priemonė konstruojant matematikos teoremų įrodymus bei
sprendžiant kai kurias aktualias praktines užduotis. Užrašyti ir įrodyti teiginiai vadinami
teoremomis, o jų verifikavimas (įrodymas) yra atliekamas naudojantis automatizuotomis ir
interaktyviomis aplinkos priemonėmis. Verifikavimas garantuoja didesnį negu testavimas
patikimumą, nes įrodomas bendras atvejis remiantis griežtais matematikos ir logikos dėsniais.
Tuo naudojasi tokios kompanijos, kaip Mitsubishi Electric Research Laboratories (MERL)
[Cou19], AbsInt [KLB+17] ir taip toliau.
Interaktyvus teoremų įrodymas Coq-e reikalauja daug pastangų, laiko ir ekspertizės. Jis
remiasi standartinėmis Coq įrodymo komandomis (vadinamomis taktikomis). Kadangi taktikos
realizuoja bazinius logikos teiginių išvedimo žingsnius, interaktyvūs įrodymai gali tapti gana
ilgi ir struktūrizuoti. Įrodymo automatizavimo lygio pakėlimas yra siektinas dalykas, bet tai
įmanoma tik pasirinkus konkretesnę uždavinių grupę ar probleminę sritį, kur įrodymo būdai ar
strategijos kartojasi. Šias įrodymo strategijas gali būtų užprogramuoti aukštesnės eilės
taktikomis, kurios padengtų žymią (ar visą) įrodymo dalį. Tokių taktikų kūrimui Coq-e
egzistuoja keletas kalbų, iš kurių populiariausia yra Ltac.
Kita ilgų Coq įrodymų, besiremiančių standartinėmis Coq taktikomis, problema - jų prastas
skaitomumas. Dažnai tokie įrodymai yra suprantami tik pačiam autoriui. Šita problema yra
nebūdinga vien tik Coq sistemai, todėl per daugelį metų buvo pasiūlyta įvairių sprendimų,
dažniausiai susijusių su deklaratyvių įrodymų kalbų kūrimu. Viena iš žinomiausių tokių kalbų
yra Isar [Wen07] kalbų grupė. Vienas iš Coq įrodymų skaitomumo problemos sprendimų būtų
dalies Isar komandų užprogramavimas naujomis Coq taktikomis.
Taigi, bakalauro baigiamojo darbo tikslas – sumažinti Coq automatizuotos teoremų įrodymų
aplinkos silpnybes pagerinant teoremų įrodymų automatizaciją bei skaitomumą.

Darbo uždaviniai yra:
1.Susipažinti su aplinka bei išmokti Coq logiką ir interaktyvaus įrodymo metodus;
2.Susipažinti ir įvaldyti įvairius naujų taktikų kūrimo būdus naudojantis Ltac kalba;
3.Naujų taktikų kūrimas Ltac priemonių pagalba siekiant pakelti įrodymo automatizavimo lygį;
4.Naujų taktikų kūrimas Ltac priemonių pagalba siekiant perkelti dalį Isar kalbos
galimybių į Coq aplinką.