Information Technology Reference
In-Depth Information
http://www.theorema.org/
and the papers cited the) and then, in the main
part of the paper, we will sketch a few ideas (which are partly implemented and
partly being implemented in Theorema) that may contribute to the other three
requirements.
2
Integration of the Functionality
of Current Mathematical Systems
Let us start from the fact that predicate logic is not only rich enough to express
any mathematical proposition but it includes also, as a sublanguage, a univer-
sal programming language and, in fact, a practical and elegant programming
language. For example, in Theorema syntax, the following formula
∀
F
(
is-Grobner-basis
[
F
]
⇔∀
f,g∈F
reduced
[
S-polynomial
[
f, g
]
,F
]=0)
(1)
can be read as a proposition (which can be proved, by the inference rules of
predicate logic, from a rich enough knowledge base
K
) but it can also be read
as an algorithm which can be applied to concrete input polynomial sets
F
, like
{
x
2
y
2
,xy
2
. Application to inputs proceeds by using a certain
simple subset of the inference rules of predicate logic, which transform
−
x
−
−
xy
+1
}
is-Grobner-basis
[
F
]
into a truth value using a knowledge base that contains elementary Grobner
bases theory and the above formula (1). (Note that Theorema uses brackets
for function and predicate application.)
Here is another example of a predicate logic formula (in Theorema syntax),
which may be read as a (recursive) algorithm:
is-sorted
[
]
∀
x
is-sorted
[
x
]
x
y
is-sorted
[
≤
∀
x,y,
z
is-sorted
[
x, y, z
]
⇔
y, z
]
.
(Formulae placed above each other should be read as conjunctions.)
In this algorithmic formula, we use “sequence variables”, which in Theo-
rema are written as overbarred identifiers: The substitution operator for se-
quence variables allows the substitution of none, one, or finitely many terms
whereas the ordinary substitution operator for the ordinary variables of predi-
cate logic (like
x
and
y
in our example) allows only the substitution of exactly
one term for a variable. Thus, for example,
is-sorted
[
1
,
2
,
2
,
5
,
7
]
,
by using the generalized substitution operator for the sequence variable
z
,may
be rewritten into
Search WWH ::
Custom Search