Rezolucja (matematyka)
Z Wikipedii, wolnej encyclopedia
Rezolucja – metoda automatycznego dowodzenia twierdzeń oparta na generowaniu nowych klauzul, aż dojdzie się do sprzeczności. W ten sposób można udowodnić, że dane twierdzenie nie jest spełnialne, lub też, co jest równoważne, że jego zaprzeczenie jest tautologią.
Ten artykuł od 2021-06 wymaga zweryfikowania podanych informacji. |
Rezolucja jest podstawą wielu praktycznych systemów dowodzenia twierdzeń rachunku predykatów pierwszego rzędu.