Logic Engineering (2)

Bijan Parsia

Propositional Resolution

• Basic AR (refutation) schema:
• Negated the goal
• Normalize
• Show unsatisfiable
• Propositional Resolution
• Negate the fomualae
• Transform into clausal form
• Derive an empty clause

Clausal Form

• Clausal form is a varient of Conjunctive Normal Form (CNF)
• CNF == a conjunction of disjunctions of literals
• A literal is a propositional letter or its negation
• I.e., P or \neg Q
• Examples
• P \land (\neg P \lor Q)
• P \land \neg P (unsatisfiable)
• (P \lor Q \lor R) \land (\neg S \lor Q \lor \neg T) \land (\neg P)
• Each conjunct is a clause.
• Clausal form
• Treat a clause as a set of literals
• \{\neg P, Q\}
• \{P, Q, R\}
• And a formula as a set of clauses
• \{\{P, Q, R\},\{\neg S, Q, \neg T\}, \{\neg P\}\}

Clausification

• Any propositional formula (or set thereof) may be reduced to clausal form.
• For example, 

• (P \land Q) \rightarrow R	Inital Formula
  \neg (P \land Q) \lor R	Implication elimination
  \neg P \lor \neg Q \lor R	De-Morgan's
  \{\neg P,  \neg Q,  R\}	Reduce to sets

• \neg((P \land Q) \rightarrow R)	Negated version
  \neg (\neg (P \land Q) \lor R)	Implication elimination
  \neg(\neg P \lor \neg Q \lor R)	De-Morgan's
  P \land  Q \land \neg R)	De-Morgan's
  \{\{\neg P\}, \{\neg Q\},  \{R\}\}	Reduce to sets

Clausification Rules

• Eliminate implication (\rightarrow, \leftrightarrow) and any other defined connectives
• e.g., (P  \rightarrow R) to (\neg P  \lor R) 
• Convert to negation normal form (NNF) via De Morgan's
• e.g., \neg (P \land Q)  to (\neg P \lor \neg Q) 
• or, \neg\neg P to P 
• Distribute all disjunctions over conjunctions
• e.g., (P  \land Q) \lor R  to (P  \lor R) \land (Q \lor R)
• Replace connectives with set notation
• Note that distribution can blow up the size of your formulae (and thus the size of your clause set!)

The Resolution Rule! (RES)

• Resolution is basically disjunctive syllogism
• I love mochi or I love cheerios
• I do not love cheerios
• Therefore, I love mochi!
• If you have two clauses with complimentary literals, you may add a new clause which is formed by deleteing the compliments from their respective clauses, and taking hte disjunction of those reduced clauses.
• The result is called the resolvent.
• The rule is easy to see with sets: \[\frac{\{\textbf{P}, Q, \neg R\}, \{\neg \textbf{P}, S, T\}}{\{Q, \neg R, S, T\}} \]
• Add the resolvent to the set of clauses and repeat!

The Empty Clause

• Apply RES to a set of (propositional) clauses until
• We derive the empty clause
• We reach a fixed point
• I.e., no matter how we apply the rule, the resolvent is already in our set of clauses
• The empty clause is  contradiction
• Why?
• Disjunction with no disjunctions (true iff one disjunct is true)
• Also, means we had unit clauses consisting of complimentary literals,\[\frac{\{\textbf{P}\}, \{\neg \textbf{P}\}}{\{\}} \]

An Example

• Does (P \land Q) \rightarrow R \models P \rightarrow (Q \rightarrow R) ?
• Deduction theorem:
• \Gamma \models \alpha  iff  \bigwedge \Gamma \rightarrow \alpha
• So, is the following a theorem (i.e., derivable from the empty set)? \[((P \land Q) \rightarrow R) \rightarrow (P \rightarrow (Q \rightarrow R))\]
• Yes! if it's negation is unsatisfiable.
• Clausal form of the negation: \[ \{\{\neg P, \neg Q, R\}^1,\{P\}^2, \{Q\}^3,\{\neg R\}^4\}\]
• Should be pretty clear how this will go
• Note that the clauses are all horn
• That is, they have at most one positive literal
• Horn propositional satisfiability is linear

Horn Thoughts

• Propositional Horn very nice computationally
• NP complete vs. Linear -- You decide!
• But 2SAT is also polynomial
• What to pick between them?
• Horn clauses are nice in other ways:
• They are conditionals: \[\{\neg P, \neg Q, \textbf{R}\} \Leftrightarrow (P \land Q) \rightarrow \textbf{R}\]
• The positive literal is the consequent.
• This looks like a rule
• R :- P, Q.
• Thus:
• Nice computational properties
• Pretty expressive
• Usable/natural

Resolution Thoughts

• Resolution is a simple rule
• Though, obviously quite powerful
• There are many parameters and variants
• Esp. in the first order case
• Generally, general resolution is fairly undirected
• So generates lots and lots of junk
• Ideally, we can focus on generating useful resolvents
• Two important strategies (esp. for Horn):
• Unit resolution (always resolve against a unit clause)
• Linear resolution (one of the resolving clauses appeared before)

Tableau (Tree) Methods

• While tableau are mainly used for description and modal logics, they work for propositional.
• Wide variety of tableau rules
• Can have many many rules
• Rules can exist for all contructors (and the negations thereof)
• Avoid the need for normalization
• But we'll do simpler rules withsome normalization
• Normalize
• Eliminate implications
• Translate to NNF
• Only appearance of negation is in literals

Propositional Tableau

• Two rules and a "clash" condition:
• "And" rule: 
• Condition: P \land Q in a branch untouched
• Action: add the conjunct(s) to the branch
• "Or" rule:
• Condition:  P \lor Q in a branch untouched
• Action: Create two branches, one with P and one with Q
• Clash rule:
• If complimentary literals appear in a branch, that branch is closed
• If all branches are closed, then the formula is unsatisfiable

Example

1. \neg((P \land Q) \rightarrow R) \rightarrow (P \rightarrow (Q \rightarrow R)) (negate)
2. (\neg P \lor \neg Q \lor R) \land (P \land Q \land \neg R) (normalize to NNF)
3. \neg P \lor \neg Q \lor R (2, and-rule)
4. \neg P \land Q \land \neg R (2, and-rule)
5. BRANCH 1: \neg P (3, or-rule)
1. P (4, and-rule) CLOSED
6. BRANCH 2: \neg Q (3, or-rule)
1. Q (4, and-rule) CLOSED
7. BRANCH 3: R (3, or-rule)
1. \neg R   (4, and-rule) CLOSED