# Item

ITEM ACTIONSEXPORT

Released

Conference Paper

#### Automated Reasoning in Extensions of Theories of Constructors with Recursively Defined Functions and Homomorphisms

##### External Ressource

http://drops.dagstuhl.de/opus/volltexte/2010/2424/

(Any fulltext)

##### Fulltext (public)

There are no public fulltexts stored in PuRe

##### Supplementary Material (public)

There is no public supplementary material available

##### Citation

Sofronie-Stokkermans, V. (2010). Automated Reasoning in Extensions of Theories of Constructors
with Recursively Defined Functions and Homomorphisms. In T. Ball, J. Giesl, R. Hähnle, & T. Nipkow (*Interaction versus Automation: the two Faces of Deduction* (pp. 1-33). Wadern: Schloss Dagstuhl.
Retrieved from http://drops.dagstuhl.de/opus/volltexte/2010/2424/pdf/09411.SofronieStokkermansViorica.Paper.2424.pdf.

Cite as: http://hdl.handle.net/11858/00-001M-0000-000F-1966-E

##### Abstract

We study possibilities of reasoning about extensions of base
theories with functions which satisfy certain recursion and
homomorphism properties. Our focus is on emphasizing
possibilities of hierarchical and modular reasoning in such
extensions and combinations thereof.
\begin{itemize}
\item[(1)] We show that the theory of absolutely free
constructors is local, and locality is preserved also in the
presence of selectors. These results are consistent with
existing decision procedures for this theory (e.g. by Oppen).
\item[(2)] We show that, under certain assumptions, extensions
of the theory of absolutely free constructors with functions
satisfying a certain type of recursion axioms satisfy locality
properties, and show that for functions with values in an
ordered domain we can combine recursive definitions with
boundedness axioms without sacrificing locality. We also address
the problem of only considering models whose data part is
the {em initial} term algebra of such theories.
\item[(3)] We analyze conditions which ensure that similar
results can be obtained if we relax some assumptions about the
absolute freeness of the underlying theory of data types, and
illustrate the ideas on an example from cryptography.
\end{itemize}
The locality results we establish allow us to reduce the task of
reasoning about the class of recursive functions we consider to
reasoning in the underlying theory of data structures (possibly
combined with the theories associated with the co-domains of
the recursive functions).
As a by-product, the methods we use provide a possibility of
presenting in a different light (and in a different form)
locality phenomena studied in cryp-to-gra-phy; we believe that
they will allow to better separate rewriting from proving, and
thus to give simpler proofs.