Information Technology Reference
In-Depth Information
as a method. If we restrict the schemes allowed in the definition of Q (and
auxiliary operations) to being recursive equalities then we arrive at the notion
of algorithmic methods.
Case Studies:
The creative potential of using schemes, together with failing proof analysis,
can only be seen in major case studies. At the moment, within the Theorema
project, three such case studies are under way: One for Grobner bases theory,
[7], one for teaching elementary analysis, and one for the theory of tuples, [8].
The results are quite promising. Notably, for Grobner bases theory, we managed
to show how the author's algorithm for the construction of Grobner bases can be
automatically synthesized from a problem specification in predicate logic. Since
the Grobner bases algorithm is deemed to be nontrivial, automated synthesis
may be considered as a good benchmark for the power of mathematical invention
methods.
Not every formula scheme is equally well suited for inventing definitions,
propositions, problems, or methods. Here are some examples of typical simple
schemes in each of the four areas:
A Typical Definition Scheme:
alternating-quantification
[
Q, P
]
Q
[
f
]
P
[
f, x, y, z
]
.
∀
P,Q
⇔∀
f
⇔∀
x
∃
y
∀
z
Many of the notions in elementary analysis (e.g. “limit”) are generated by
this (and similar) schemes.
A Typical Proposition Scheme:
is-homomorphic
[
f, g, h
]
⇔∀
x,y
(
h
[
f
[
x, y
]] =
g
[
h
[
x
]
,h
[
y
]])
.
∀
f,g,h
Of course, all possible ”algebraic” interactions (describable by equalities be-
tween various compositions) of functions are candidates for proposition schemes.
A Typical Problem Scheme:
explicit-problem
[
A, P, Q
]
.
P
[
A
[
x
]]
Q
[
x, A
[
x
]]
∀
A,P,Q
⇔∀
x
This seems to be one of the most popular problem schemes: Find a method
A
that produces, for any
x
, a “standardized” form
A
[
x
] (that satisfies
P
[
A
[
x
]])
such that
A
[
x
] is still in some relation (e.g. equivalence)
Q
with
x
.(Examples:
sorting problem, problem of constructing Grobner bases, etc.)
Two Typical Algorithm Schemes:
divide-and-conquer
[
F, c, s, g, h
1
,h
2
]
.
⇔
F
[
x
]=
s
[
x
]
otherwise
⇐
c
[
x
]
∀
F,c,s,g,h
1
,h
2
g
[
F
[
h
1
[
x
]]
,F
[
h
2
[
x
]]]
⇐
Search WWH ::
Custom Search