Reals
(theory Reals
:smt-lib-version 2.6
:smt-lib-release "2017-11-24"
:written-by "Cesare Tinelli"
:date "2010-04-17"
:last-updated "2017-05-08"
:update-history
"Note: history only accounts for content changes, not release changes.
2017-05-08 Fixed error in note on intepretation of (/t 0).
2016-04-20 Minor formatting of notes fields.
2015-04-25 Updated to Version 2.5.
2012-06-20 Modified the definition of :value attribute to include abstract values
for irrational algebraic numbers.
"
:sorts ((Real 0))
:funs ((NUMERAL Real)
(DECIMAL Real)
(- Real Real) ; negation
(- Real Real Real :left-assoc) ; subtraction
(+ Real Real Real :left-assoc)
(* Real Real Real :left-assoc)
(/ Real Real Real :left-assoc)
(<= Real Real Bool :chainable)
(< Real Real Bool :chainable)
(>= Real Real Bool :chainable)
(> Real Real Bool :chainable)
)
:values
"The set of values for the sort Real consists of
- an abstract value for each irrational algebraic number
- all numerals
- all terms of the form (- n) where n is a numeral other than 0
- all terms of the form (/ m n) or (/ (- m) n) where
- m is a numeral other than 0,
- n is a numeral other than 0 and 1,
- as integers, m and n have no common factors besides 1.
"
:definition
"For every expanded signature Sigma, the instance of Reals with that
signature is the theory consisting of all Sigma-models that interpret
- the sort Real as the set of all real numbers,
- each numeral as the corresponding real number,
- each decimal as the corresponding real number,
- / as a total function that coincides with the real division function
for all inputs x and y where y is non-zero,
- the other function symbols of Reals as expected.
"
:notes
"Since in SMT-LIB logic all function symbols are interpreted as total
functions, terms of the form (/ t 0) *are* meaningful in every
instance of Reals. However, the declaration imposes no constraints
on their value. This means in particular that
- for every instance theory T and
- for every value v (as defined in the :values attribute) and
closed term t of sort Real,
there is a model of T that satisfies (= v (/ t 0)).
"
:notes
"The restriction of Reals over the signature having just the symbols
(0 Real)
(1 Real)
(- Real Real)
(+ Real Real Real)
(* Real Real Real)
(<= Real Real Bool)
(< Real Real Bool)
coincides with the theory of real closed fields, axiomatized by
the formulas below:
- associativity of +
(forall ((x Real) (y Real) (z Real))
(= (+ (+ x y) z) (+ x (+ y z))))
- commutativity of +
(forall ((x Real) (y Real))
(= (* x y) (* y x)))
- 0 is the right (and by commutativity, left) unit of +
(forall ((x Real)) (= (+ x 0) x))
- right (and left) inverse wrt +
(forall ((x Real)) (= (+ x (- x)) 0))
- associativity of *
(forall ((x Real) (y Real) (z Real))
(= (* (* x y) z) (* x (* y z))))
- commutativity of *
(forall ((x Real) (y Real)) (= (* x y) (* y x)))
- 1 is the right (and by commutativity, left) unit of *
(forall ((x Real)) (= (* x 1) x))
- existence of right (and left) inverse wrt *
(forall ((x Real))
(or (= x 0) (exists (y Real) (= (* x y) 1))))
- left distributivity of * over +
(forall ((x Real) (y Real) (z Real))
(= (* x (+ y z)) (+ (* x y) (* x z))))
- right distributivity of * over +
(forall ((x Real) (y Real) (z Real))
(= (* (+ x y) z) (+ (* x z) (* y z))))
- non-triviality
(distinct 0 1)
- all positive elements have a square root
(forall (x Real)
(exists (y Real) (or (= x (* y y)) (= (- x) (* y y)))))
- axiom schemas for all n > 0
(forall (x_1 Real) ... (x_n Real)
(distinct (+ (* x_1 x_1) (+ ... (* x_n x_n)))
(- 1)))
- axiom schemas for all odd n > 0 where (^ y n) abbreviates
the n-fold product of y with itself
(forall (x_1 Real) ... (x_n Real)
(exists (y Real)
(= 0
(+ (^ y n) (+ (* x_1 (^ y n-1)) (+ ... (+ (* x_{n-1} y) x_n)))))))
- reflexivity of <=
(forall (x Real) (<= x x))
- antisymmetry of <=
(forall (x Real) (y Real)
(=> (and (<= x y) (<= y x))
(= x y)))
- transitivity of <=
(forall (x Real) (y Real) (z Real)
(=> (and (<= x y) (<= y z))
(<= x z)))
- totality of <=
(forall (x Real) (y Real)
(or (<= x y) (<= y x)))
- monotonicity of <= wrt +
(forall (x Real) (y Real) (z Real)
(=> (<= x y) (<= (+ x z) (+ y z))))
- monotonicity of <= wrt *
(forall (x Real) (y Real) (z Real)
(=> (and (<= x y) (<= 0 z))
(<= (* z x) (* z y))))
- definition of <
(forall (x Real) (y Real)
(= (< x y) (and (<= x y) (distinct x y))))
References:
1) W. Hodges. Model theory. Cambridge University Press, 1993.
2) PlanetMath, http://planetmath.org/encyclopedia/RealClosedFields.html
"
)
(
raw file)