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.
Articles by others on the same topic
There are currently no matching articles.