9. fejezet - Következtetés elsőrendű logikában

Ebben a fejezetben definiálunk egy olyan hatékony következtetési mechanizmust, amelyik képes megválaszolni az elsőrendű logikában feltett kérdéseket.

A 7. fejezetben meghatároztuk a következtetés (inference) fogalmát, és bemutattuk, hogy hogyan érhető el helyes és teljes következtetés az ítéletlogikában. Ebben a fejezetben kiterjesztjük ezeket az eredményeket, hogy olyan algoritmusokat kapjunk, amelyek bármely, az elsőrendű logikában feltehető kérdésre válaszolni tudnak. Ez jelentős eredmény, mivel az elsőrendű logikával többé-kevésbé mindent kifejezhetünk, ha elég alaposan végezzük a feladatot.

A 9.1. alfejezet következtetési szabályokat vezet be a kvantorokra, és megmutatja, hogy hogyan lehet – jóllehet nagy erőfeszítések árán – az elsőrendű logikai következtetést ítéletlogikai következtetésre redukálni. A 9.2. alfejezet leírja az egyesítés (unification) ötletét, bemutatva, hogy az egyesítés felhasználásával, hogyan alkothatunk következtetési szabályokat, amelyek közvetlenül az elsőrendű logikai mondatokra alkalmazhatók. Ezután a 9.3. alfejezetben megvizsgáljuk az elsőrendű logikai algoritmusok három nagy családját: az előrefelé láncolást (forward chaining) és ennek alkalmazását a deduktív adatbázisokban (deductive databases) és a produkciós rendszerekben (production systems). A hátrafelé láncolást (backward chaining) és a logikai programozást (logic programming) alkalmazó rendszereket a 9.4. alfejezetben tárgyaljuk; míg a rezolúció alapú tételbizonyító (theorem-proving) rendszereket a 9.5. alfejezet ismerteti. Általánosságban mindig a leghatékonyabb, az adott feladatban reprezentálandó tényeket és axiómákat kezelni képes módszert próbáljuk használni. A teljesen általános, a tetszőleges elsőrendű logikai mondatokon alkalmazható rezolúciós következtetés általában kevésbé hatékony, mint a bizonyos típusú mondatokon alkalmazható előre- vagy hátrafelé láncolást használó megoldások.