Current Slide
Small screen detected. You are viewing the mobile version of SlideWiki. If you wish to edit slides you will need to use a larger device.
Resolution - Principle
- Resolution commonly requires sentences to be in clause normal form (also called conjunctive normal form or CNF)
- A clause is a disjunction of literals (implicitly universally quantified)
- E.g. : l1 ∨ … ∨ ln
- A formula in clause normal form conjunction of a set of clauses
- E.g.: C1 ∧ … ∧ Cn = (ln ∨ … ∨ lm) ∧ … ∧ (li ∨ … ∨ lj)
- High level steps in a resolution proof:
- Put the premises or axioms into clause normal form (CNF)
- Add the negation of the to be proven statement, in clause form, to the set of axioms
- Resolve these clauses together, using the resolution rule , producing new clauses that logically follow from them
- Derive a contradiction by generating the empty clause.
- The substitutions used to produce the empty clause are those under which the opposite of the negated goal is true
Speaker notes:
Content Tools
Tools
Sources (0)
Tags (0)
Comments (0)
History
Usage
Questions (0)
Playlists (0)
Quality
Sources
There are currently no sources for this slide.