Inductive generalization and proofs of functions properties

The paper presents a formal system and an inductive method for proving function properties and investigates the relationships between inductive and deductive proofs. Induction is performed by stepwise generalizing specific given elements of function domains which are known to satisfy the property itself. The method is based on symbolic computation, reflexivity lemmas and function behaviour estimate, and is proven sound when functions and predicates belong to a constructively defined class. Finally, an example is completely worked out.