On the EA-style integrated processing of self-contained mathematical texts
| Data(s) |
2001
|
|---|---|
| Resumo |
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. |
| Formato |
application/postscript |
| Identificador |
http://calcium.dcs.kcl.ac.uk/892/1/ao_calculemus.ps 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 |
| Publicador |
A K Peters |
| Relação |
http://calcium.dcs.kcl.ac.uk/892/ |
| Tipo |
Book Section PeerReviewed |
