PUMA
Istituto di Scienza e Tecnologie dell'Informazione     
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


Icona documento 1) Download Document PDF


Icona documento Open access Icona documento Restricted Icona documento Private

 


Per ulteriori informazioni, contattare: Librarian http://puma.isti.cnr.it

Valid HTML 4.0 Transitional