Presná definícia
Čo znamená dokazovanie viet?
Dokazovanie viet automaticky alebo interaktívne hľadá formálny dôkaz, že cieľová formula vyplýva z axióm podľa povolených inferenčných pravidiel. Úspešný dôkaz garantuje vzťah v danom formálnom systéme, nie pravdivosť axióm o svete. Prover môže tiež hľadať kontramodel alebo vrátiť neznámy stav.
Skúsenosť a kontext
Ako sa pojem používa v praxi
Pri verifikácii protokolu sa vlastnosti a predpoklady formalizujú a prover vytvorí strojovo kontrolovateľný dôkaz. Tím recenzuje preklad požiadaviek, minimalizuje axiómy a uchová verziu solvera. Timeout sa neinterpretuje ako nepravda.
Overiteľnosť
Odborné zdroje
Praktické odpovede
Často kladené otázky
Ako funguje dokazovanie viet?
Vyhľadávanie aplikuje rezolúciu, prepisovanie alebo kalkul sekventov na odvodenie cieľa či rozporu z negovaného cieľa.
Kedy má dokazovanie viet praktický význam?
Pri verifikácii protokolu sa vlastnosti a predpoklady formalizujú a prover vytvorí strojovo kontrolovateľný dôkaz.
S čím si pojem nezamieňať?
SAT solver rozhoduje splniteľnosť výrokovej formuly; theorem prover môže pracovať s kvantifikátormi a produkovať dôkaz všeobecnej vety.
Ako sa výsledok kontroluje?
Kontroluje sa dôkaz nezávislým kernelom, konzistencia axióm, kontramodely, časový limit a pokrytie požiadaviek.
Na čo si dať pozor?
Chybná formalizácia dokáže inú vetu než používateľ zamýšľal a neukončenie alebo timeout nedáva záver o platnosti.