Model Checker

Domain

Example: a , b , c

Constants

Constant
Denotes (domain element)
Format: c denotes element a. Leave empty if none.

Symbols

Symbol
Arity
Extension / Value

Arity 0: enter T or F (propositional constant).
Arity 1: elements, e.g. a,b (unary predicate).
Arity 2–3: tuples, e.g. <a,b>, <b,a> or <a,b,c>, <b,c,a>.

Sentence

ASCII shorthands OK: -> (→), ~ (¬), /\ (∧), \/ (∨), or “and/or/not”.