Aiello L., Aiello M., Attardi G., Prini G. PPC (Pisa Proof Checker): a tool for experiments in proof theory and mathematical theory of computation. Apparso anche in: Universta' degli Studi di Pisa, Istituto di scienze dell'informazione, note scientifiche, luglio 1975. Agosto 1975. Internal note IEI-B75-12, 1975. |

Abstract (English) |
The paper describes a research in progress. The research consists i the construction of a system for generating proofs of theorems in an interactive way with the help of a computer. The system is described in some detail. The ideas inspiring it are presented, as well as the underlying logic and a bunch of examples taken from the Mathematical Theory of Computation. Considerations are made on further developments of the system in two main directions: i) extension of the logic to increase its expressive power and implementation of other logics; ii) extension of th proving capability of the system. The first extension requires an analysis of the fields of application foreseen for the system, while the second one requires an accurate analysis of the most commonly used strategies for building proofs. This is possible only after a long experimentation on the use of the system. | |

Subject |

1) Download Document PDF |

Open access Restricted Private