This is an old revision of the document!
Finite Model Finders
Consider formulas of first order logic (recall Predicate Logic Informally).
A model of is an interpretation in which is true.
We can define these notions precisely: First-Order Logic.
For a given bound , is there an interpretation of a given formula with a domain of size ?
This problem is decidable.
Finite model finder: a tool that searches for such models.
Approaches:
- encoding into SAT (popular recently because SAT solvers are good): MACE, Paradox, KodKod (used in Alloy)
- generalize SAT algorithms to search for finite domains and not just propositional ones (SEM)