Paskevich A. Methods of formalisation of mathematical knowledge and reasoning: theoretical and practical aspects.

In the thesis, we study and develop means of presentation of mathematical knowledge as well as schemes of mathematical reasoning. Our research is aimed at constructing a system for automated processing of formalized mathematical texts; in particular, for verifying the text's claims. The texts being processed are written in a formal language which is close to the natural language of real-life mathematical publications. Proof search is held on two levels of reasoning: the upper one tries to make large proof steps by applying traditional reasoning schemes - it simplifies the initial proof task and splits it into smaller subgoals; the lower one "closes" the generated subgoals using an exhaustive combinatorial inference search in some deductive formalism. In the first chapter of the thesis, the language ForTheL, intended for representation of formalized mathematical texts, is developed. The syntax of a ForTheL follows the rules of English grammar (though, of course, just a small fragment of English is formalized). Affirmations in ForTheL can be supplied with proofs; special proof schemes like proof by contradiction, by case analysis, or by general induction are allowed. Sentences and ections of ForTheL can be translated into first-order formulas with a series of syntactical transformations. We also introduce a relation of logical precedence between ForTheL sections and define a procedure of proof normalization. In the second chapter, we define different levels of ForTheL text's correct-ness and describe procedures for correctness verification. In order to reason about parts of complex formulas, we introduce the notion of a locally true statement, a statement which can be considered true in a given position inside a given formula. We show that ordinarily valid statements are also locally valid anywhere in any surrounding formula. We introduce a local analogue of the modus ponens rule and prove its soundness. Finally, it is shown that a locally true equivalence is a sufficient condition for an equivalent replacement of a subformula or a subterm. The latter property gives us theoretical ground for definition expansion steps or for applications of simplifying lemmas. A ForTheL text is said to be ontologically correct whenever the domain of any symbol occurring in the text is properly defined and, in any occurrenc e of such a symbol, its arguments fall into this domain. Note that the second part of this definition which deals with individual occurrences can be precisely expressed in terms of local validity. A ForTheL text is said to be correct whenever every claim in the text (after proof normalization) follows from its logical predecessors. Then we describe the verification procedure and a number of heuristic proof methods used on the upper level of the system to transform and simplify proof search tasks before passing them to the lower level, a combinatorial prover. In the third chapter, we formulate a goal-driven tableau calculus GDT which doesn't require preliminary skolemization and uses the notion of ad-missiblesubstitution instead. This calculus is proved to be sound and com-plete with respect to Model Elimination, a classical clause tableau calculus. Then we introduce an original goal-driven tableau calculus LPCT with lazy paramodulation rules and prove its completeness in the classical first-order logic with equality. The results of the thesis are implemented in a software system for auto-mated processing and verification of formal mathematical texts. This system, called SAD (System for Automated Deduction) includes ForTheL parser and translator, procedures for checking ontological and general text correctness, routines for collecting facts about particular occurrences of terms, for definition expansion and simplification of compound goals. SAD also includes a prover for classical first-order logic with equality based on the GDT calculus. The proposed approach was approved in a series of experiments with non-trivial real-life mathematical texts that were formalized in ForTheL and then verified with SAD. These texts include Infinite and Finite Ramsey Theorems and the proof of the fact that the square root of a prime number is irrational.