Let be a signature and the set of terms over . The set of symbols for is the disjoint union of and , a countably infinite set whose elements are called variables. Now, adjoin the set , assumed to be disjoint from . An atomic formula over is any one of the following:
either , where and are terms in ,
or , where is an -ary relation symbol, and .
A literal is a formula that is either atomic or of the form where is atomic. If a literal is atomic, it is called a positive literal. Otherwise, it is a negative literal.
A finite disjunction of literals is called a clause. In other words, a clause is a formula of the form , where each is a literal.
A qunatifier-free formula is a formula that does not contain the symbols or .
If we identify a formula with its double negation , then it can be shown that any quantifier-free formula can be identified with a formula that is in conjunctive normal form, that is, a finite conjunction of clauses. For a proof, see this link (http://planetmath.org/EveryPropositionIsEquivalentToAPropositionInDNF)
|Date of creation||2013-03-22 12:42:54|
|Last modified on||2013-03-22 12:42:54|
|Last modified by||CWoo (3771)|
|Synonym||quantifier free formula|