A coherent formula is built from atomic relations and equality using , , finite conjunction, finite disjunction and existential quantification. General negation and universal quantification are not constructors. Substitution of well-typed terms preserves coherent formulas.
New to topics? Read the docs here!