Lecturecise 21: Some Decidable Logics of Sets and Relations
Continuing Lecturecise 20
Finish example for ground and non-ground resolution: pdf
Effectively Propositional Logic (EPR) and Importance of Finite Herbrand Universe
- exists x1,…,xn. forall y1,…,ym. G
- only relation symbols and constants allowed
- Skolemization gives only constants, so the set of ground terms finite (bounded by number of original constants + existentials)
Deciding Quantifier-Free Set Algebra by Reduction to EPR
- represent set inclusion using universal quantifier
- non-inclusion gives existential quantifier
- Skolemization turns all existential into constants, because there are no universal variables above them