On the EA-Style Integrated Processing of Self-Contained Mathematical Texts
Anatoli I. Degtyarev, Alexander V. Lyaletski, Marina K. Morokhovets · 2000
In this paper , we continue to develop our approach to theorem proof search in the EA-style, that is theorem proving in the frame-work of integrated processing mathematical texts written in a 1st-order formal language close to the natural language used in mathematical papers. This framework enables constructing a sound and complete goal-oriented sequent-type calculus with “large-block” inference rules. In particular, it contains the formal analogs of such natural proof search techniques as definition handling and auxiliary proposition application. The calculus allows to incorporate symbolic computations in an inference search.