MPI-INF Logo
Publications

Server    domino.mpi-inf.mpg.de

Proceedings Article, Paper
@InProceedings
Beitrag in Tagungsband, Workshop

Author, Editor
Author(s):
Sofronie-Stokkermans, Vioricadblp
Editor(s):
Schmidt, Renate A.dblp
Not MPII Editor(s):
Schmidt, Renate A.
BibTeX cite key*:
Sofronie-Stokkermans-cade09
Title, Booktitle
Title*:
Locality results for certain extensions of theories with bridging functions
Booktitle*:
Automated Deduction - CADE-22 : 22nd International Conference on Automated Deduction
Event, URLs
Conference URL::
http://complogic.cs.mcgill.ca/cade22/
Downloading URL:
http://dx.doi.org/10.1007/978-3-642-02959-2_5
Event Address*:
Montreal, Canada
Language:
English
Event Date*
(no longer used):
Organization:
Event Start Date:
2 August 2009
Event End Date:
7 August 2009
Publisher
Name*:
Springer
URL:
http://www.springer-ny.com/
Address*:
Berlin, Germany
Type:
Vol, No, Year, pp.
Series:
Lecture Notes in Artificial Intelligence
Volume:
5663
Number:
Month:
Pages:
67-83
Year*:
2009
VG Wort Pages:
ISBN/ISSN:
978-3-642-02958-5
Sequence Number:
DOI:
10.1007/978-3-642-02959-2_5
Note, Abstract, ©
(LaTeX) Abstract:
n this paper we study possibilities of reasoning about
functions over theories of data types which satisfy
certain recursion (or homomorphism) properties, with a
focus on emphasizing possibilities of hierarchical and
modular reasoning in such extensions and combinations thereof.

We start by considering theories of absolutely free data
structures, and continue by studying extensions of such
theories with selectors, with functions which attach scalar
data to the data structures and with additional functions
defined using a certain type of recursion axioms (possibly
having values in a different -- e.g.\ numeric -- domain).
We show that in these cases locality results can be established.
This allows us to reduce the task of reasoning about the class
of recursive functions we consider to reasoning in the
underlying theory of absolutely free data structures
(resp. in a combination of the theory of absolutely free data
structures with the theory attached with the domains of the
additional functions). We then show that similar results can be
obtained if we relax some assumptions about the absolute
freeness of the underlying theory of data types. We investigate
the applications of these ideas in verification and cryptography.
Download
Access Level:
Public

Correlation
MPG Unit:
Max-Planck-Institut für Informatik
MPG Subunit:
Automation of Logic
Appearance:
MPII WWW Server, MPII FTP Server, MPG publications list, university publications list, working group publication list, Fachbeirat, VG Wort



BibTeX Entry:

@INPROCEEDINGS{Sofronie-Stokkermans-cade09,
AUTHOR = {Sofronie-Stokkermans, Viorica},
EDITOR = {Schmidt, Renate A.},
TITLE = {Locality results for certain extensions of theories with bridging functions},
BOOKTITLE = {Automated Deduction - CADE-22 : 22nd International Conference on Automated Deduction},
PUBLISHER = {Springer},
YEAR = {2009},
VOLUME = {5663},
PAGES = {67--83},
SERIES = {Lecture Notes in Artificial Intelligence},
ADDRESS = {Montreal, Canada},
ISBN = {978-3-642-02958-5},
DOI = {10.1007/978-3-642-02959-2_5},
}


Entry last modified by Manuel Lamotte-Schubert, 03/16/2011
Hide details for Edit History (please click the blue arrow to see the details)Edit History (please click the blue arrow to see the details)

Editor(s)
[Library]
Created
04/22/2009 01:56:07 PM
Revisions
4.
3.
2.
1.
0.
Editor(s)
Manuel Lamotte-Schubert
Anja Becker
Anja Becker
Viorica Sofronie-Stokkermans
Viorica Sofronie-Stokkermans
Edit Dates
16.03.2011 15:21:16
15.03.2011 09:55:23
25.03.2010 12:57:53
03/05/2010 10:26:50 AM
04/22/2009 01:56:07 PM