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.
1979
Istituto di informatica e telematica - IIT
Istituto di Scienza e Tecnologie dell'Informazione "Alessandro Faedo" - ISTI
Primitive recursive functions
Inductive reasoning
Generalization
Symbolic computation
Program properties
Function behaviour estimate
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.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/20.500.14243/379323
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? ND
social impact