PLATO: A Tool to Assist Programming as Term Rewriting and Theorem Proving

SAMPAIO A.; HAEBERER, ARMANDO MARTIN; TERRA C.; URURAHY, C.; FRIAS, MARCELO FABIAN; ALBUQUERQUE N.

LECTURE NOTES IN COMPUTER SCIENCE

Springer

Año: 1995 vol. 915 p. 797 - 798

0302-9743

In this paper we present PLATO, a tool designed for theory presentation construction, theorem proving and formula derivation. It was motivated by equational algebraic theory manipulation needs, nevertheless its aim is software development by program calculation. PLATO has applications in algebra — boolean algebra, relation algebra, etc. — and mathematical logic — as a general framework for theorem proving under different logics —. In the field of software development, we show its application in program calculi construction and in program development under these calculi.