Differences
This shows you the differences between two versions of the page.
|
sav08:deciding_quantifier-free_fol [2008/04/23 06:49] vkuncak |
sav08:deciding_quantifier-free_fol [2015/04/21 17:30] |
||
|---|---|---|---|
| Line 1: | Line 1: | ||
| - | ====== Deciding Quantifier-Free First-Order Logic Formulas ====== | ||
| - | |||
| - | Given a FOL formula with equality and without quantifiers, we wish to check whether it is satisfiable (does there exist an interpretation that makes this formula true). | ||
| - | |||
| - | We do not restrict ourselves to any particular class of structures, we look at all possible structures. | ||
| - | |||
| - | Based on what we learned so far, how can we solve this problem? ++|Skolemize.++ ++|Apply paramodulation (see [[Definition of resolution for FOL]] and [[Proof Rule for Equality]].) ++ | ||
| - | |||
| - | Example: is the following formula satisfiable: | ||
| - | \[ | ||
| - | a=f(a) \land a \neq b | ||
| - | \] | ||
| - | is the following | ||
| - | \[ | ||
| - | (f(a)=b \lor (f(f(f(a))) = a \land f(a) \neq f(b))) \land f(f(f(f(a)) \neq b \land b=f(b) | ||
| - | \] | ||