Proceedings Article, Paper
@InProceedings
Beitrag in Tagungsband, Workshop


Show entries of:

this year (2019) | last year (2018) | two years ago (2017) | Notes URL

Action:

login to update

Options:




Library Locked Library locked




Author, Editor

Author(s):

Sofronie-Stokkermans, Viorica

dblp



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

URL of the conference:

http://complogic.cs.mcgill.ca/cade22/

URL for downloading the paper:

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
Show details for Edit History (please click the blue arrow to see the details)Edit History (please click the blue arrow to see the details)
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
Show details for Attachment SectionAttachment Section
Hide details for Attachment SectionAttachment Section