The System for Automated Deduction (SAD) by Andrei Paskevich et. al. is an automatic proof-checker that can process fairly natural mathematical input statements and short texts. We have recently made signi cant improvements to the system: speed-ups of the checking algorithms allow handling of chapter-sized texts with an argumentative granularity comparable to textbook mathematics; extensions of the input language provide native support of basic notions like sets and functions; SAD input can now be written in a LATEX style which typesets like ordinary mathematical text. Based on experiences and examples so far we expect to be able to write natural textbook-style mathematics which can be automatically checked for proof correctness. Actually this paper is a proof-checked SAD document itself.
but leaving much room for further improvements. Revising the checking algorithms we were able to cut down some proof-checking times from minutes to seconds. This allows the handling of chapter-sized texts and libraries of interlinked texts. The rudimentary support of sets was replaced by stronger mechanisms for sets and functions.
3
is included in a forthel environment, marked by a vertical line in the margin. Only text embedded within such environments is parsed and proof-checked by SAD. We present an actual working example from complex analysis which proves the familiar maximum principle for holomorphic functions from other basic theorems. 4
[number/-s][ontored on][checkontored on]
De nition 1. A subset of M is a set N such that every element of N is an element of M . De nition 2. Assume M is a subset of the domain of f . f [M ] = ff [x] j x 2 M g.
Signature 1. A complex number is a notion. Let z; w denote complex numbers.
Axiom 1. Every element of Dom(f ) is a complex number and for every element z of Dom(f ) f [z] is a complex number.
Axiom 2. Every element of M is a complex number.
Signature 2. A real number is a notion. Let x; y denote real numbers.
Signature 3. jzj is a real number.
Signature 4. x is positive is an atom. Let ; denote positive real numbers.
Signature 5. x < y is an atom. Let x
y stand for x = y or x < y.
Axiom 3. x < y ! :y < x.
Signature 6. f is holomorphic is an atom.
Signature 7. B (z) is a set that contains z.
Axiom 4. jzj < jwj for some element w of B (z).
Axiom 5. B (z) is open.
De nition 3. M is open i for every element z of M there exists such that B (z) is a subset of M .
De nition 4. A local maximal point of f is an element z of the domain of f such that there exists such that B (z) is a subset of the domain of f and jf [w]j jf [z]j for every element w of B (z).
De nition 5. Let U be a subset of the domain of f . f is constant on U i there exists z such that f [w] = z for every element w of U . Let f is constant stand for f is constant on the domain of f . 5
Axiom 6 (OpenMappingTheorem). Assume f is holomorphic and B (z) is a subset of the domain of f . If f is not constant on B (z) then f [B (z)] is open.
Signature 8. A region is an open set.
Axiom 7 (IdentityTheorem). Assume f is holomorphic and the domain of f is a region. Assume that B (z) is a subset of the domain of f . If f is constant on B (z) then f is constant. 6
Theorem 1. Assume f is holomorphic and the domain of f is a region. If f has a local maximal point then f is constant.
for every element w of B (z).
that B (f [z]) is a subset of f [B (z)]. Therefore there exists an element w of B (z) such that jf [z]j < jf [w]j.
We make some comments which also describe important aspects of the ForTheL-language: 1. This text is typeset from a LATEX- le which is also accepted and proof-checked by the improved SAD within a few seconds. The complete le starts out with basic de nitions and axioms for the argument and is about three times the size of the excerpt. 2. The text is formulated in the restricted natural language ForTheL, which is immediately understandable by mathematicians. The language is apparently translatable to rst-order logic, but it is more exible and natural than just using logical connectives. There is, e.g., some typing and use of anonymous variables like in the de nition: \a subset of M is a set N such that every element of N is an element of M ". 3. The language constructs of ForTheL have been carefully modelled after OLM to allow elegant formulations of logical dependencies without (nested) brackets or other formal devices. 4. ForTheL allows to freely introduce new unde ned notions by signature commands and specify their properties by axioms, without worrying about grounding everything in some foundational system like set theory. Other notions may be based on previous notions by de nitions. 5. The attentive reader will have noticed that some notions and axioms are formulated just for the example and would have to be amended if we want to capture the situation in more generality: In the text, e.g., " and are ranging over positive real numbers. This notion has only been introduced in the ad hoc preliminaries, and positivity has not been connected with the <-relation since that is not required for the proof of the maximum principle. A more comprehensive text would of course have to x that liberal approach.
readers attention to a \small world" delineated by the types in the statements under immediate consideration.
ontological checks that terms belong to certain types. Ontological checking has similarities with strong type checking for programming languages, and it helps to nd formalization errors.
in a text. In the example above we nd notions such as \set", \complex number", \real number" and \positive real number". A variable must be declared to belong to some notion before it can be used. Moreover, we can not quantify unboundedly but only over notions. The translation to rst-order logic is done using type guards.
usually not be considered when dealing with a problem of number theory. Being integer is then an ontological property rather than a logical one. Within the world of integers it cannot substantially contribute to an argument.
every application of a predicate or function symbol is well-de ned. When introducing a symbol to the signature, an author makes certain assumptions on its arguments, which we call domain conditions. These assumptions may be hidden in a text through the use of pretyped variables. For example, in De nition 2 in the above text we introduce the symbol [ ](f; M ) with the domain conditions aSet(M ); aFunction(f ); aSubsetOf(M; Dom(f )).
Signature. A real number is a notion.
Signature. x y is a real number.
Signature. x is nonzero is an atom.
Signature. Assume x is nonzero. x 1 is a real number. Axiom. Assume x and y are nonzero. x y is nonzero.
Axiom. Assume x is nonzero. x 1 is nonzero.
(aRealNumber(x) ^ aRealNumber(y)) ! (isNonzero(x) ^ isNonzero(y)) ! isNonzero(x y) aRealNumber(x) ! isNonzero(x) ! isNonzero(x 1):
condition for () 1. Therefore for the rst formula, the most general domain condition is (aRealNumber(x) ^ aRealNumber(y) and for the second formula it is aRealNumber(x) ^ isNonzero(x). We can thus reduce these formulas to isNonzero(x) ^ isNonzero(y) ! isNonzero(x y) isNonzero(x 1):
well-de ned. We call the procedure ontological reduction.
Theorem 2. Let T be an ontologically correct ForTheL text. Assume that the rst-order image of T has a model in which all domain conditions are non-empty. Then its ontological reduction also has a model.
interpretation of symbols outside of their domain, so that domain guards become super uous. Ontological correctness ensures that after those changes we still have a model of the original text.
many-sorted rst-order logic. It will in general not be a problem, since usual mathematical symbols are de ned for non-empty domains. In case where a text uses hypotheticals to nally show emptyness of a certain class, possibly problematic domain conditions can be excluded from the reduction process to ensure soundness.
and polymorphic) many-sorted FOL to pure FOL are developed for Sledgehammer in order to encode Isabelle's type system. Encoding by type guards, the approach formerly used by SAD, was among the worst performing.
sorted FOL, then the result is very close to that obtained by the \featherweigth guards" encoding described in [BBPS13]. However, our approach is more exible and therefore better suited for our soft type system. For example we can possibly delete predicates of arity higher than one and negated predicates. Furthermore, we can more adequately deal with the complex relations between ForTheL notions. 8
ization workbench. We shall use the Isabelle editor as an IDE for formalizing mathematics and for giving more feedback to the user. The compact Haskell source code of SAD is being systematized and documented to ensure the sustainability of the project. We shall try to better separate the parsing from the proof-checking process so that the language module could be used with other formal mathematics systems.
mar. Natural language words should not be arbitrary letter combinations, as is possible now, but taken from an
and inductive data types. Standard domains like number systems will be formalized in a basic library of texts useful for many purposes. Some aspects like the handling of natural numbers could be taken over into the software, to provide some computational power. Also our term rewriting system will be improved.
shall also examine research articles whether a partial formulation in ForTheL is pro table. To evaluate usability, students of mathematics will be asked to prepare homework solutions in the system.
Texts about various domains can be arranged in interlinked libraries. The above example could be linked to an introductory text about holomorphic functions, which again could be linked to some development of complex numbers etc. Texts could be linked by a simple reading-in of other texts, or by more sophisticated, truth-preserving operations like uni cations of notations, or they might require some logical bridging between conclusions of one text and premisses of the other. In our example text, the notion of a region is introduced to allow standard formulations of the Identity Theorem and the Maximum Principle. We only require regions to be open, whereas in a comprehensive foundation regions also have to be connected and non-empty. To connect our example to such a foundational text requires the implication that a region is open. A systematic study of such relations is required for building larger libraries. 9
becomes nearly indistinguishable from the natural language of a domain. The convergence of the formal and the natural leads to a host of serious questions, ranging from practical to philosophical issues. In any case our research demonstrates that the formal approach in mathematics is not restricted to foundations but that it can be used all the way up to sophisticated theories provided that the formalism is set up prudently in a hierarchical fashion.
We conjecture that in a few years time it will be routinely possible to formulate substantial textbook mathematics and some advanced mathematics in a ForTheL-like controlled and proof-checked natural language. Other proof assistants could similarly be equipped with natural language input. Formal mathematics could be carried out naturally in a text-orientated way, using collections of interlinked texts which are readable and understandable by men and machines.