And Tree Example - Model Elimination

determining if a formula is a consequence of a set of formulas

have a set of clauses → generate subproblems of it from it.

Steps

• Start with no predicate → everything is possible
• Pick a clause & see if it can be true with all other clauses

basically going to go through each one of the clauses, and explore a version of that world where we assign true to part of that clause. All our clauses are OR together.

Goal: at least one of the final expansions to be solved means contradiction aka negation

Example

Start with empty world

pick one of these that hasn't been used yet in that expansion path.
We pick $p V q$ → create two versions of the world. One is P true, the other is Q true

imagine we have a good search control, we would target sth has -p there are only 3rd and 4th clause. we pick 3rd

The first one is solvable, pick that, got contradiction since p & -p cant exist together → return yes

Next solve the other ones

both are solvable, p & -p and q & -q

solve the other ones