One Approach to Automated Proof of Mathematical Assertions

摘要

We describe the method of theorems proofs search in environment of an all-in-one mathematical text. The approach is based on the sequential logical calculus of the first order. It contains formal analogues of such natural methods of proofs search as expanding of definitions and application of auxiliary statements or lemmas.