License: 
Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/DagSemProc.09411.3
URN: urn:nbn:de:0030-drops-24241
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2010/2424/
|
Go to the corresponding Portal |
Sofronie-Stokkermans, Viorica
Automated reasoning in extensions of theories of constructors with recursively defined functions and homomorphisms
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.
BibTeX - Entry
@InProceedings{sofroniestokkermans:DagSemProc.09411.3,
author = {Sofronie-Stokkermans, Viorica},
title = {{Automated reasoning in extensions of theories of constructors with recursively defined functions and homomorphisms}},
booktitle = {Interaction versus Automation: The two Faces of Deduction},
pages = {1--33},
series = {Dagstuhl Seminar Proceedings (DagSemProc)},
ISSN = {1862-4405},
year = {2010},
volume = {9411},
editor = {Thomas Ball and J\"{u}rgen Giesl and Reiner H\"{a}hnle and Tobias Nipkow},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2010/2424},
URN = {urn:nbn:de:0030-drops-24241},
doi = {10.4230/DagSemProc.09411.3},
annote = {Keywords: Decision procedures, recursive datatypes, recursive functions, homomorphisms, verification, cryptography}
}
|
Keywords: |
|
Decision procedures, recursive datatypes, recursive functions, homomorphisms, verification, cryptography |
|
Collection: |
|
09411 - Interaction versus Automation: The two Faces of Deduction |
|
Issue Date: |
|
2010 |
|
Date of publication: |
|
09.03.2010 |
