One Approach to Automated Proof of Mathematical Assertions
Anatoli I. Degtyarev, Alexander V. Lyaletski, Marina K. Morokhovets · Journal of Automation and Information Sciences · 2000
We describe the method of theorems proofs search in evironment 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.