|
||||||||
Resolution in ML - Python Automation and Machine Learning for ICs - - An Online Book - |
||||||||
Python Automation and Machine Learning for ICs http://www.globalsino.com/ICs/ | ||||||||
Chapter/Index: Introduction | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | Appendix | ||||||||
================================================================================= Resolution is a powerful inference rule used in propositional logic and first-order logic to derive new clauses from existing ones. In automated theorem proving, resolution is often employed in proof methods such as the Resolution Refutation. The basic idea of resolution is to resolve two clauses by finding a complementary pair of literals, one positive and one negative, and then resolving or eliminating them. The resolution step results in a new clause that combines the remaining literals. The resolution rule can be formally stated as follows: Suppose we have two clauses: where ,
The resolution of C1 and C2 is the clause: where, Res(C1, C2) is obtained by removing both P and ¬P from C1 and C2 and combining the remaining literals. Resolution is often used in automated theorem proving to show the unsatisfiability of a set of clauses. The process involves repeatedly applying the resolution rule until either a contradiction is derived (e.g., an empty clause), indicating the unsatisfiability of the original set of clauses, or the process cannot proceed further.
============================================
|
||||||||
================================================================================= | ||||||||
|
||||||||