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