Algoritmusok a tételbizonyításban
Dátum
2009-05-08T09:16:55Z
Szerzők
Folyóirat címe
Folyóirat ISSN
Kötet címe (évfolyam száma)
Kiadó
Absztrakt
Automatikus tételbizonyítás az ítéletlogikában. A Davis-Putnam algoritmus. Rezolúciós kalkulus. Konjunkciós normálformává alakítás. KNF minimalizálása Quine-McCluskey-algoritmussal.
Leírás
Kulcsszavak
rezolúció, normálforma, KNF, minimalizálás