atomic formula
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:
-
1.
either , where and are terms in ,
-
2.
or , where is an -ary relation symbol, and .
Remarks.
-
1.
Using atomic formulas, one can inductively build formulas using the logical connectives , , , etc… In this sense, atomic formulas are formulas that can not be broken down into simpler formulas; they are the building blocks of formulas.
-
2.
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.
-
3.
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.
-
4.
A qunatifier-free formula is a formula that does not contain the symbols or .
-
5.
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)
Title | atomic formula |
Canonical name | AtomicFormula |
Date of creation | 2013-03-22 12:42:54 |
Last modified on | 2013-03-22 12:42:54 |
Owner | CWoo (3771) |
Last modified by | CWoo (3771) |
Numerical id | 10 |
Author | CWoo (3771) |
Entry type | Definition |
Classification | msc 03C99 |
Classification | msc 03B10 |
Synonym | quantifier free formula |
Related topic | TermsAndFormulas |
Related topic | CNF |
Related topic | DNF |
Defines | literal |
Defines | clause |
Defines | quantifier-free formula |
Defines | positive literal |
Defines | negative literal |