Řešení LP rezoluční metodou

• Rezoluční metoda:

• odvození sporem

• odvoditelnost je ekvivalentní odvození prázdné klauzule (NIL) v ostatních případech nelze říci, zdali je klauzule odvoditelná

• Princip: A1Ai  B1 C1CjB2

• pomocí unifikace: substitucemi se snažíme dosáhnout toho, aby B1 a B2 byly komplementární

• odvození rezolventy: je-li po unifikaci tvar vstupu A1AiB C1CjB, pak lze odvodit A1AiC1Cj