CnfAtom | R Documentation |
CnfAtom
objects represent a single statement that is used to build up CNF formulae.
They are mostly intermediate, created using the %among%
operator or CnfAtom()
directly, and combined into CnfClause
and CnfFormula
objects.
CnfClause
and CnfFormula
do not, however, contain CnfAtom
objects directly,
CnfAtom
s contain an indirect reference to a CnfSymbol
by referencing its name
and its CnfUniverse
. They furthermore contain a set of values. An CnfAtom
represents a statement asserting that the given symbol takes up one of the
given values.
If the set of values is empty, the CnfAtom
represents a contradiction (FALSE).
If it is the full domain of the symbol, the CnfAtom
represents a tautology (TRUE).
These values can be converted to, and from, logical(1)
values using as.logical()
and as.CnfAtom()
.
CnfAtom
objects can be negated using the !
operator, which will return the CnfAtom
representing set membership in the complement of the symbol with respect to its domain.
CnfAtom
s can furthermore be combined using the |
operator to form a CnfClause
,
and using the &
operator to form a CnfFormula
. This happens even if the
resulting statement could be represented as a single CnfAtom
.
This is part of the CNF representation tooling, which is currently considered experimental; it is for internal use.
CnfAtom(symbol, values)
e1 %among% e2
as.CnfAtom(x)
symbol |
( |
values |
( |
e1 |
( |
e2 |
( |
x |
(any) |
We would have preferred to overload the %in%
operator, but this is currently
not easily possible in R. We therefore created the %among%
operator.
The internal representation of a CnfAtom
may change in the future.
A new CnfAtom
object.
Other CNF representation objects:
CnfClause()
,
CnfFormula()
,
CnfSymbol()
,
CnfUniverse()
u = CnfUniverse()
X = CnfSymbol(u, "X", c("a", "b", "c"))
CnfAtom(X, c("a", "b"))
X %among% "a"
X %among% character(0)
X %among% c("a", "b", "c")
as.logical(X %among% character(0))
as.CnfAtom(TRUE)
!(X %among% "a")
X %among% "a" | X %among% "b" # creates a CnfClause
X %among% "a" & X %among% c("a", "b") # creates a CnfFormula
Add the following code to your website.
For more information on customizing the embed code, read Embedding Snippets.