A list of clauses is a list of not empty clauses separated by comma.
A clause is a not empty list of litterals separated by spaces or line breaks.
A litteral (examples : p, -q, -r(x,y)) is a term preceded or not by the minus sign.
A term is an identifier followed or not followed by a list of terms in parentheses separated by comma.
A term that is an identifier starting with one of the character a up to f and that is within another term is a constant. Within the litterals p(a), -c(b,x), the identifiers a and b are constants.
-----------------------------------------------------------------------------------------------------------------
In this context, from a prover by "model elimination", whose theoretical basis is described here in English and French, a literal is also called a B-literal and a clause is also called a elementary chain.

examples | syntax | info | home | download

Last Modified : 02-Dec-2019