public final class Quantifier extends AbstractSortedOperator
Modifier and Type | Field and Description |
---|---|
static Quantifier |
ALL
the usual 'forall' operator 'all' (be A a formula then
'all x.A' is true if and only if for all elements d of the
universe A{x<-d} (x substituted with d) is true
|
static Name |
ALL_NAME |
static Quantifier |
EX
the usual 'exists' operator 'ex' (be A a formula then
'ex x.A' is true if and only if there is at least one elements
d of the universe such that A{x<-d} (x substituted with d) is true
|
static Name |
EX_NAME |
Modifier | Constructor and Description |
---|---|
private |
Quantifier(Name name) |
additionalValidTopLevel, additionalValidTopLevel2, argSort, argSorts, sort, sort
arity, bindVarsAt, isRigid, name, toString, validTopLevel, whereToBind
clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait
arity, bindVarsAt, isRigid, validTopLevel
public static final Name ALL_NAME
public static final Name EX_NAME
public static final Quantifier ALL
public static final Quantifier EX
private Quantifier(Name name)