Finite satisfiability problem for first-order logic (source code)

= Finite satisfiability problem for first-order logic

The finite satisfiability problem asks whether a first-order sentence has a finite model. It is computably enumerable because finite structures and their truth relations can be searched effectively.