English
 
Help Privacy Policy Disclaimer
  Advanced SearchBrowse
  1. Item Summary / 
  2. View item

Item

ITEM ACTIONSEXPORT
Add to Basket
 Local TagsRelease HistoryDetailsSummary
  Locality results for certain extensions of theories with bridging functions

Sofronie-Stokkermans, V. (2009). Locality results for certain extensions of theories with bridging functions. In R. A. Schmidt (Ed.), Automated Deduction - CADE-22. Berlin: Springer.

Item is

 

show all hide all

Basic

show hide
Item Permalink: https://hdl.handle.net/11858/00-001M-0000-000F-1A62-E Version Permalink: https://hdl.handle.net/11858/00-001M-0000-0024-BBA1-C
Genre: Conference Paper

Files

show Files

Locators

show

Creators

show
hide
 Creators:
Sofronie-Stokkermans, Viorica1, Author           
Affiliations:
1Automation of Logic, MPI for Informatics, Max Planck Society, ou_1116545              

Content

show
hide
Free keywords: -
 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.

Details

show
hide
Language(s): eng - English
 Dates: 2009-04-222009
 Publication Status: Issued
 Pages: -
 Publishing info: -
 Table of Contents: -
 Rev. Type: -
 Identifiers: eDoc: 521086
Other: Local-ID: C125716C0050FB51-33993A1B73DCBEECC12575A000419048-Sofronie-Stokkermans-cade09
DOI: 10.1007/978-3-642-02959-2_5
 Degree: -

Event

show
hide
Title: CADE 2009
Place of Event: Montreal, Canada
Start-/End Date: 2009-08-02 - 2009-08-07

Legal Case

show

Project information

show

Source 1

show
hide
Title: Automated Deduction - CADE-22
  Subtitle : 22nd International Conference on Automated Deduction, Montreal, Canada, August 2-7, 2009. Proceedings
  Abbreviation : CADE 2009
Source Genre: Proceedings
 Creator(s):
Schmidt, Renate A.1, Editor           
Affiliations:
1 Programming Logics, MPI for Informatics, Max Planck Society, ou_40045            
Publ. Info: Berlin : Springer
Pages: - Volume / Issue: - Sequence Number: - Start / End Page: - Identifier: -

Source 2

show
hide
Title: Lecture Notes in Artificial Intelligence
  Abbreviation : LNAI
Source Genre: Series
 Creator(s):
Affiliations:
Publ. Info: -
Pages: - Volume / Issue: 5663 Sequence Number: - Start / End Page: - Identifier: -