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.
Inductive generalization and proofs of functions properties
1979
Abstract
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.File in questo prodotto:
File | Dimensione | Formato | |
---|---|---|---|
prod_422008-doc_149963.pdf
solo utenti autorizzati
Descrizione: Inductive generalization and proofs of functions properties
Tipologia:
Versione Editoriale (PDF)
Dimensione
3.45 MB
Formato
Adobe PDF
|
3.45 MB | Adobe PDF | Visualizza/Apri Richiedi una copia |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.