In the frame of the Theorema project a software system is developed on
the basis Mathematica that supports the automated generation of
mathematical proofs. The emphasis lies on producing proofs in a style
that comes close to the style in which human mathematicians write down
their proofs. At the same time, an input language based on usual
predicate logic is being developed, which also allows input in a form
like mathematicians are used to from scientific publishing.
General prove techniques that have their application in virtually all
fields of mathematics must be provided by the system, such as
propositional logic proving, predicate logic proving, set theory
proving, proving with case distinctions, induction over various domains,
etc. Moreover, the system must be well designed from a usability point
of view, because otherwise potential users cannot be encouraged to use
the system. Thus, this part of the Theorema project deals with user
interface design, general system engineering for keeping the system
maintainable as it is steadily growing, and improvement of general
methods that are not tailored for particular areas of mathematics.

Sprache der Kurzfassung:

Deutsch

Englische Bezeichnung:

PROVE

Englische Kurzfassung:

In the frame of the Theorema project a software system is developed on
the basis Mathematica that supports the automated generation of
mathematical proofs. The emphasis lies on producing proofs in a style
that comes close to the style in which human mathematicians write down
their proofs. At the same time, an input language based on usual
predicate logic is being developed, which also allows input in a form
like mathematicians are used to from scientific publishing.
General prove techniques that have their application in virtually all
fields of mathematics must be provided by the system, such as
propositional logic proving, predicate logic proving, set theory
proving, proving with case distinctions, induction over various domains,
etc. Moreover, the system must be well designed from a usability point
of view, because otherwise potential users cannot be encouraged to use
the system. Thus, this part of the Theorema project deals with user
interface design, general system engineering for keeping the system
maintainable as it is steadily growing, and improvement of general
methods that are not tailored for particular areas of mathematics.