Electronic Proceedings Article
@InProceedings
Internet-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):

Ball, Thomas
Giesl, Jürgen
Hähnle, Reiner
Nipkow, Tobias

dblp
dblp
dblp
dblp

Not MPII Editor(s):

Ball, Thomas
Giesl, Jürgen
Hähnle, Reiner
Nipkow, Tobias

BibTeX cite key*:

Sofronie-Stokkermans-dagstuhl-2010

Title, Conference

Title*:

Automated reasoning in extensions of theories of constructors with recursively defined functions and homomorphisms-

Booktitle*:

Interaction versus Automation : the two Faces of Deduction

Event Address*:

Schloss Dagstuhl

URL of the conference:


Event Date*:
(no longer used):


URL for downloading the paper:

http://drops.dagstuhl.de/opus/volltexte/2010/2424/pdf/09411.SofronieStokkermansViorica.Paper.2424.pdf

Event Start Date:

4 October 2009

Event End Date:

9 October 2009

Language:

English

Organization:


Publisher

Publisher's Name:

Schloss Dagstuhl - Leibniz-Zentrum für Informatik

Publisher's URL:


Address*:

Dagstuhl

Type:


Vol, No, pp., Year

Series:

Dagstuhl Seminar Proceedings

Volume:

09411

Number:


Month:


Pages:

1-33



Sequence Number:


Year*:

2010

ISBN/ISSN:

1862-4405





Abstract, Links, ©

URL for Reference:


Note:


(LaTeX) 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.

URL for the Abstract:

http://drops.dagstuhl.de/portals/abstract.php?id=2424



Tags, Categories, Keywords:


HyperLinks / References / URLs:

urn:nbn:de:0030-drops-24241

Copyright Message:


Personal Comments:


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-dagstuhl-2010,
AUTHOR = {Sofronie-Stokkermans, Viorica},
EDITOR = {Ball, Thomas and Giesl, J{\"u}rgen and H{\"a}hnle, Reiner and Nipkow, Tobias},
TITLE = {Automated reasoning in extensions of theories of constructors with recursively defined functions and homomorphisms-},
BOOKTITLE = {Interaction versus Automation : the two Faces of Deduction},
PUBLISHER = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik},
YEAR = {2010},
VOLUME = {09411},
PAGES = {1--33},
SERIES = {Dagstuhl Seminar Proceedings},
ADDRESS = {Schloss Dagstuhl},
ISBN = {1862-4405},
}


Entry last modified by Anja Becker, 03/15/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
03/09/2010 02:45:04 PM
Revisions
6.
5.
4.
3.
2.
Editor(s)
Anja Becker
Anja Becker
Anja Becker
Anja Becker
Anja Becker
Edit Dates
15.03.2011 13:28:40
18.02.2011 13:30:58
07.02.2011 12:40:19
07.02.2011 12:39:20
07.02.2011 12:39:07
Show details for Attachment SectionAttachment Section
Hide details for Attachment SectionAttachment Section