Aiello L., Weyhrauch R. Using meta-theoretic reasoning to do algebra. In: 5th Conference on Automated Deduction (Les Arcs, Francia, 8-11 Luglio 1980). Proceedings, vol. 87 pp. 1 - 13. (Lecture Notes in Computer Science). Springer, 1980. |

Abstract (English) |
We report on an experiment in interactive reasoning with FOL. The subject of the reasoning is elementary algebra. The main point of the paper is to show how the use of metatheoretic knowledge results in improving the quality of the resulting proofs in that, in this environment, they are both easier to find and easier to understand. | |

Subject |

1) Download Document PDF |

Open access Restricted Private