# 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