LARA

Exercise 14

Slides:

Combining FOL Models

Summary:

  • SAT + theories
  • lazy approach and eager approach
  • small models and Ackerman encoding
  • quantifier instantiation

Deciding Quantifier-Free FOL

Deciding Quantifier-Free FOL over Ground Terms

Arithmetic and Eager Encoding

References