Aiello L., Aiello M., Attardi G., Prini G. PPC (Pisa Proof Checker): a tool for experiments in theorem proving and mathematical theory of computation. In: Fundamenta Informaticae, vol. 1 (2) pp. 251 - 275. IOS Press, 1977. |

Abstract (English) |
An interactive proof checker is a system which is ab1e of building a formal proof (in some deductive calculus) by executing commands provided by the user. Proof checkers are useful both for making experiments in proof construction within various formal systems and for proving theorems in those fields of mathematics (such as mathematical theory of computation) where proofs are necessarily very large and unfeasible by hand. Two levels may be distinguished in a proof checker. The lower one implements the proof management routines, and is independent of any particular logic. The higher one implements the inference ru1es of a particular logical calculus. Powerful higher level rules are also needed to make the use of the checker practical. Almost all routine steps may be then generated automatically, and the user has just to give some "hints" to the checker, which transforms an "informal argument" into a formal proof. | |

Subject | Automatic theorem proving Denotational semantics of programming languages Mathematical theory of computation Proof of formal properties of programs |

1) Download Document PDF |

Open access Restricted Private