Deutsch
 
Hilfe Datenschutzhinweis Impressum
  DetailsucheBrowse

Datensatz

DATENSATZ AKTIONENEXPORT
 
 
DownloadE-Mail
 Lokale TagsFreigabegeschichteDetailsÜbersicht
  Automated Reasoning in Extensions of Theories of Constructors with Recursively Defined Functions and Homomorphisms

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 (Eds.), 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.

Item is

 

einblenden: alle ausblenden: alle

Basisdaten

einblenden: ausblenden:
Datensatz-Permalink: https://hdl.handle.net/11858/00-001M-0000-000F-1966-E Versions-Permalink: https://hdl.handle.net/11858/00-001M-0000-0028-39E3-9
Genre: Konferenzbeitrag

Externe Referenzen

einblenden:
ausblenden:
externe Referenz:
http://drops.dagstuhl.de/opus/volltexte/2010/2424/ (beliebiger Volltext)
Beschreibung:
-
OA-Status:

Urheber

einblenden:
ausblenden:
 Urheber:
Sofronie-Stokkermans, Viorica1, Autor           
Affiliations:
1Automation of Logic, MPI for Informatics, Max Planck Society, ou_1116545              

Inhalt

einblenden:
ausblenden:
Schlagwörter: -
 Zusammenfassung: 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.

Details

einblenden:
ausblenden:
Sprache(n): eng - English
 Datum: 2010
 Publikationsstatus: Online veröffentlicht
 Seiten: -
 Ort, Verlag, Ausgabe: -
 Inhaltsverzeichnis: -
 Art der Begutachtung: -
 Identifikatoren: eDoc: 536348
URI: http://drops.dagstuhl.de/opus/volltexte/2010/2424/pdf/09411.SofronieStokkermansViorica.Paper.2424.pdf
Anderer: Local-ID: C125716C0050FB51-36DE00D5AA94A519C12576E1004B89B9-Sofronie-Stokkermans-dagstuhl-2010
 Art des Abschluß: -

Veranstaltung

einblenden:
ausblenden:
Titel: Interaction versus Automation: The two Faces of Deduction (Dagstuhl Seminar 09411)
Veranstaltungsort: Schloss Dagstuhl, Wadern
Start-/Enddatum: 2009-10-04 - 2009-10-09

Entscheidung

einblenden:

Projektinformation

einblenden:

Quelle 1

einblenden:
ausblenden:
Titel: Interaction versus Automation : the two Faces of Deduction
Genre der Quelle: Konferenzband
 Urheber:
Ball, Thomas1, Herausgeber
Giesl, Jürgen1, Herausgeber
Hähnle, Reiner1, Herausgeber
Nipkow, Tobias1, Herausgeber
Affiliations:
1 External Organizations, ou_persistent22            
Ort, Verlag, Ausgabe: Wadern : Schloss Dagstuhl
Seiten: - Band / Heft: - Artikelnummer: - Start- / Endseite: 1 - 33 Identifikator: -

Quelle 2

einblenden:
ausblenden:
Titel: Dagstuhl Seminar Proceedings
  Kurztitel : DSP
Genre der Quelle: Reihe
 Urheber:
Affiliations:
Ort, Verlag, Ausgabe: -
Seiten: - Band / Heft: 09411 Artikelnummer: - Start- / Endseite: - Identifikator: ISSN: 1862-4405