Kovásznai Gergely: "Ennek az ostoba gépnek még bizonyítania kell!"
Az emberiség régi álma, hogy gondolkodó gépeket alkosson. Már eleve
vitatható ennek a célkitűzésnek az értelme. De a célkitűzés létezik. Az
biztos, hogy a megvalósításához először is modellezni kell az emberi
gondolkodás folyamatát, erre tettek kísérletet többek között a logikával
foglalkozó matematikusok.
A különböző logikákra kalkulusokat dolgoztak
ki, melyek segítségével következtetéseket tudunk végezni, kérdéses
igazságokat bizonyítani vagy cáfolni. A kalkulusok közül külön figyelmet
érdemelnek az automatikus következtetési szabályokkal rendelkezők. Ezek
adják az alapját az automatikus tételbizonyító programoknak, melyek
következtetőmotorjai sok-sok szakértői rendszernek, azaz olyan
informatikai rendszereknek, ahol egy adott tárgyterület tényanyagából
kell kikövetkeztetni kérdéses vagy új igazságokat.
A tablómódszerek
iránya az egyik lehetséges irány ebben a témában. Meg
fogom mutatni, hogy a
tablók, melyek tulajdonképpen gráfok (általában
fák vagy DAG-ok) milyen
sokrétűen használhatók sok-sok célra a
tételbizonyításban. Azt is érdemes
lenne megvizsgálni, hogy az elmúlt
évtizedekben jelentős kutatott és
fejlesztett rezolúciós tételbizonyítás
mi módon ötvözhető a tablókkal, és ha
igen, akkor mit nyerhetünk ezzel
és amit nyerünk, megéri-e?
