Mechanization Of General Topology And Related Problems In Automatic Deduction Based On Isabelle

Mathematics Mechanization is intended to study mathematical problems in a constructive and algorithmic manner so that the computation, reasoning or proving of these mathematical problems can be fulfilled mechanically or even au-tomatically. The mechanization of mathematical problems requires that each step in the computation or proof be followed by a definitely specified next step, and finally the conclusion can be reached along the specified steps. Automated the-orem proving is one of the most important tasks in Mathematics Mechanization, and mainly studys how to apply computer programs on proving mathematical theorems, or, more specifically, how to formalize the process of human reasoning and proving into a series of procedures that can be manipulated and executed automatically on computers.As one of the theoretical foundations of modern mathematics, topology is a major area of mathematics concerned with properties that are preserved un-der continuous deformations of objects. However, the abstract objects studied in topology are too difficult to express in computer systems, which leads to a slow development in automated theorem proving of topology.The rapid development in computer technology and theorem proving tools has opened up the possibilities of implementation of topological automated the-orem proving. Isabelle, also known as a theorem proof assistant, is a generic interactive theorem prover jointly developed by L.C. Paulson and T. Nipkow in1986. Using natural deduction rules, Isabelle provides a generic framework for developing theorem proving systems. It not only supports formalized represen-tation of mathematical formulas, but also supplies a reasoning tool for logical for-mula deduction. The λ-calculus with types makes Isabelle an efficient reasoning tool with enriched expressiveness, powerful rule libraries, flexible and extensible tactic libraries.General Topology is a basic branch of Topology and provides a common foundation for the other branches of Topology, for example, algebraic topology, geometric topology, and differential topology. The main work of the thesis con-sists of the following three parts:Firstly, we present formalized expression and theorem proving of General Topology. We formalize in high-order logic the abstract notions in General Topol-ogy, such as topological spaces, open sets, closed sets, neighborhoods, closures and continuous maps, and translate them into computable functions. An au-tomated theorem proof can then be generated by the construction of proof tactic sequences and stepwise refinement. During the proving process, a lot of methods and techniques such as introduction tactic, rewrite tactic, case tactic have been introduced, and we implement the automated proofs for numerous fundamen-tal theorems in General Topology, for example, the Pasting Lemma, Kuratowski theorems and C. T. Yang’s theorem, which involves complicated set computation.Secondly, based on the mechanization of General Topology, we propose for-malized expression and theorem proving of Topological Dynamics. We formalize in high-order logic the abstract definitions in Topological Dynamics, such as topo-logical groups, topological transformation groups, topological dynamic systems, invariant sets, and construct automatic proofs for some fundamental theorems.Thirdly, we develop an Isabelle-based tool of formal proofs script, Isabelle-Helper, to find (or help find) theorem proofs and generate proof scripts. This tool is essentially an expert system of automated theorem proving. It remarkably decreases the search space and improves the proving efficiency, by constructing libraries of mathematical theorems and of theorem proving tactics and by classi-fying the tactic libraries according to the distance between formulas. Automated theorem proofs are generated through search, match making and combination in the libraries of theorems and tactics. The tool also supplies the user some proof assistance, such as the generation of complete theorem proof scripts, a hint of the proof in the next step and etc. In addition, IsabelleHelper integrates Isabelle and Maple through mathematical service buses. Isabelle is a type system which aims to construct both human-readable and machine-checkable theorem proofs. However, it usually renders redundant proofs for complicated problems where algebraic computations are involved. By contrast, Maple, as a computer algebra system concentrating on symbolic computation, is able to carry on flexible and efficient calculation and deduction, but may lead to incorrect or invalid proofs due to lack of a unified verification mechanism. In view of the pros and cons of these two proving systems, we implement an integration of Isabelle and Maple based on Mule, an open-source SOA framework, which improves the proving capabilities and scope of Isabelle.