English
 
Help Privacy Policy Disclaimer
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT
 
 
DownloadE-Mail
 DetailsSummary
  Unification in Order-Sorted Logic with Term Declarations

Socher-Ambrosius, R. (1993). Unification in Order-Sorted Logic with Term Declarations. In A. Voronkov (Ed.), Proceedings of the 4th Conference on Logic Programming and Automated Reasoning (LPAR-93) (pp. 301-308). Berlin, Germany: Springer.

Item is

 

show all hide all

Basic

show hide
Item Permalink: https://hdl.handle.net/11858/00-001M-0000-0014-ADED-9 Version Permalink: https://hdl.handle.net/11858/00-001M-0000-0014-ADEE-7
Genre: Conference Paper

Files

show Files

Locators

show

Creators

show
hide
 Creators:
Socher-Ambrosius, Rolf1, Author           
Affiliations:
1Programming Logics, MPI for Informatics, Max Planck Society, ou_40045              

Content

show
hide
Free keywords: -
 Abstract: This paper provides two results concerning Order-Sorted Logic with Term Declarations. First, we show that linear term declarations can be transformed conservatively into function declarations, thus yielding elementary signatures. This provides a simple proof of the well known fact that unification in linear signatures is decidable. A similar transformation exists for semi-linear term declarations, resulting in shallow term declarations. Secondly, we provide an inference system transforming sort constraints over an arbitrary signature into almost solved form. The step from almost solved forms to solved forms requires a procedure to decide emptiness of sort intersections, which is not possible in general. This shows that it is the sort intersection problem that accounts for the undecidability of unification in signatures with term declarations.

Details

show
hide
Language(s): eng - English
 Dates: 2010-03-121993
 Publication Status: Issued
 Pages: -
 Publishing info: Berlin, Germany : Springer
 Table of Contents: -
 Rev. Type: -
 Identifiers: eDoc: 519567
Other: Local-ID: C1256104005ECAFC-90B7B5F4B7F73AD1C125614400623676-Socher93a
 Degree: -

Event

show
hide
Title: Untitled Event
Place of Event: St. Petersburg, Russia
Start-/End Date: 1993

Legal Case

show

Project information

show

Source 1

show
hide
Title: Proceedings of the 4th Conference on Logic Programming and Automated Reasoning (LPAR-93)
Source Genre: Proceedings
 Creator(s):
Voronkov, Andrei1, Editor           
Affiliations:
1 Programming Logics, MPI for Informatics, Max Planck Society, ou_40045            
Publ. Info: Berlin, Germany : Springer
Pages: - Volume / Issue: - Sequence Number: - Start / End Page: 301 - 308 Identifier: -

Source 2

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