A 3TAP tételbizonyító ismertetése

Abstract

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.