|Home Latest Advanced Search By Year By Division|
|Not Logged in. Login|
On the EA-style integrated processing of self-contained mathematical texts
Degtyarev, Anatoli and Lyaletski, Alexander and Morokhovets, Marina (2001) On the EA-style integrated processing of self-contained mathematical texts. In: Symbolic computation and automated reasoning. A K Peters, pp. 126-141. ISBN 1-56881-145-4
A sound and complete first-order goal-oriented sequent-type calculus is developed with ``large-block'' inference rules. In particular, the calculus contains formal analogues of such natural proof-search techniques as handling definitions and applying auxiliary propositions.
Repository Staff Only: item control page