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

Postscript - Repository staff only - Requires a viewer, such as GSview
168Kb

Abstract

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.

Item Type:	Book Section
Subjects:	UNSPECIFIED
ID Code:	892
Deposited By:	Dr Anatoli Degtyarev
Deposited On:	08 Nov 2007 08:32
Last Modified:	08 Nov 2007 08:32

Repository Staff Only: item control page

Accessibility | Terms and Conditions | Last Modified 01 November 2007