A system which induces properties of functions is presented. Induction is performed by step-wise generalizing specific given elements of the function domains for which the system can test that the property holds. The system relies on symbolic computation, reflexivity lemmas, and an estimate of the behaviour of the functions. Finally, the paper gives a basis for an evaluation of the system by constructively defining a class of theorems which the system is able to induce. "In mathematics as in physical sciences we may use observation and induction to discover general laws, But there is a difference. In the physical sciences, there is no higher authority than observation and induction, but in mathematics there is such an authority: rigorous proof" G. Polya How to solve. it. Doubleday (New York, 1957).
Inducing Function Properties from Computation Traces
SIROVICH, Franco
1979-01-01
Abstract
A system which induces properties of functions is presented. Induction is performed by step-wise generalizing specific given elements of the function domains for which the system can test that the property holds. The system relies on symbolic computation, reflexivity lemmas, and an estimate of the behaviour of the functions. Finally, the paper gives a basis for an evaluation of the system by constructively defining a class of theorems which the system is able to induce. "In mathematics as in physical sciences we may use observation and induction to discover general laws, But there is a difference. In the physical sciences, there is no higher authority than observation and induction, but in mathematics there is such an authority: rigorous proof" G. Polya How to solve. it. Doubleday (New York, 1957).
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
