The paper presents a non-standard theorem prover which uses both deduction and induction in proving program properties. The method first instantiates the variables occurring in the property to suitable data structure as far as the instantiated property could be proven by reducing it to "true". Secondly, to the instantiated property an inductive step is applied, which possibly gives back the property itself or a generalization of . If the inductive step succeeds, and if the property and the involved functions belong to a sub-class of primitive recursive functions for which the inductive step is proven sound, the theorem is established. Although the proposed theorem prover is not complete, yet a great deal of program properties belong to the above sub-class. Moreover, a complete theorem prover can fruitfully use it as an auxiliary tool, since it always requires a limited and srnall amount of time and space.
A Non-Standard Theorem Prover
SIROVICH, Franco
1982-01-01
Abstract
The paper presents a non-standard theorem prover which uses both deduction and induction in proving program properties. The method first instantiates the variables occurring in the property to suitable data structure as far as the instantiated property could be proven by reducing it to "true". Secondly, to the instantiated property an inductive step is applied, which possibly gives back the property itself or a generalization of . If the inductive step succeeds, and if the property and the involved functions belong to a sub-class of primitive recursive functions for which the inductive step is proven sound, the theorem is established. Although the proposed theorem prover is not complete, yet a great deal of program properties belong to the above sub-class. Moreover, a complete theorem prover can fruitfully use it as an auxiliary tool, since it always requires a limited and srnall amount of time and space.
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
