Model Checker
Describe a finite structure, then ask whether a closed sentence is true in it.
Domain
The elements the structure is built from, separated by commas.
Constants
Which element each name picks out. Leave empty if the language has no constants.
Constant
Denotes
Symbols
Each predicate, its arity, and what it is true of.
Symbol
Arity
Extension / value
Arity 0 takes T or F.
Arity 1 takes elements, e.g. a,b.
Arity 2–3 take tuples, e.g. <a,b>, <b,a>.
Sentence
A closed sentence to evaluate in the structure above.
ASCII shorthands work: -> for →, ~ for ¬,
/\ for ∧, \/ for ∨.