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