LARA

This is an old revision of the document!

Finite Model Finders

Consider formulas of first order logic (recall Predicate Logic Informally).

A model of $F$ is an interpretation in which $F$ is true.

We can define these notions precisely: First-Order Logic.

For a given bound $k$, is there an interpretation of a given formula with a domain of size $k$?

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)

References