A 3TAP tételbizonyító ismertetése
A 3TAP tételbizonyító ismertetése
Fájlok
Dátum
2007-02-19T09:27:45Z
Szerzők
Márai, Pál
Folyóirat címe
Folyóirat ISSN
Kötet címe (évfolyam száma)
Kiadó
Absztrakt
A tételbizonyítók (theorem provers, avagy automatikus következtetők) két dologban
különböznek a logikai programozási nyelvektől (logic programming languages).
Először is, a logikai programozási nyelvek többsége csak Horn-klózokat képes kezelni,
míg a tételbizonyítók a teljes elsőrendű logikát elfogadják. Másrészt, a Prolog programok összefogják a logikát és a vezérlést. A programozó azon választása, hogy A ( B;C helyett A ( C;B kifejezést ír, befolyásolja a program végrehajtását. Tételbizonyítók esetében
a felhasználó ezek bármelyikét leírhatja, vagy egy másik formát, mint a :B ( C; :A
és az eredmény mindig pontosan ugyanaz lesz. A tételbizonyítóknak is szükségük van
vezérlési információra a hatékony működés érdekében, de ez az információ a tudásbázistól elkülönítve tárolódik, és nem a tudásreprezentáció része. A tételbizonyítók területén végzett kutatás jelentős része az általánosan használható vezérlési stratégiák megtalálására koncentrál.
Leírás
Kulcsszavak
mesterséges intelligencia, automatikus tételbizonyítás, elsőrendű logika, talókalkulus, analitikus tabló