(theory Reals_Int
:written_by {Cesare Tinelli}
:date {08/04/05}
:updated {30/01/09}
:history {
30/01/09 removed erroneous :assoc attribute for binary minus
}
:sorts (Real)
:notes
"The (unsupported) annotations of the function/predicate symbols have
the following meaning:
attribute | possible value | meaning
-------------------------------------------------------
:assoc // the symbol is associative
:comm // the symbol is commutative
:iden a constant c c is the symbol left and right unit
:trans // the symbol is transitive
:refl // the symbol is reflexive
:irref // the symbol is irreflexive
:antisym // the symbol is antisymmetric
"
:funs ((0 Real)
(1 Real)
(~ Real Real) ; unary minus
(- Real Real Real) ; binary minus
(+ Real Real Real :assoc :comm :unit {0})
(* Real Real Real :assoc :comm :unit {1})
)
:preds ((<= Real Real :refl :trans :antisym)
(< Real Real :trans :irref)
(IsInt Real)
)
:definition
"This theory extends the theory Reals with an IsInt predicate symbol.
More precisely, this is the first-order theory of the real numbers structure
that interprets the (IsInt _) predicate as the unary relation coiciding with
the set of all the integer numbers.
"
:notes
"Note that this theory is not (recursively) axiomatizable in a first-order logic such
as SMT-LIB's underlying logic (this is simply because the integers are not first-order
axiomatizable).
"
)