Journal Article
@Article
Artikel in Fachzeitschrift


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(s)

Author(s):

Horbach, Matthias
Weidenbach, Christoph

dblp
dblp



BibTeX cite key*:

HorbachWeidenbach2010

Title

Title*:

Superposition for Fixed Domains

Journal

Journal Title*:

ACM Transactions on Computational Logic

Journal's URL:


Download URL
for the article:

http://doi.acm.org/10.1145/1805950.1805957

Language:

English

Publisher

Publisher's
Name:

ACM

Publisher's URL:


Publisher's
Address:

New York, NY

ISSN:

1529-3785

Vol, No, pp, Date

Volume*:

11

Number:

4

Publishing Date:

November 2010

Pages*:

27,1-27,35

Number of
VG Pages:

67

Page Start:

27,1

Page End:

27,35

Sequence Number:

27

DOI:

10.1145/1805950.1805957

Note, Abstract, ©

Note:


(LaTeX) Abstract:

Disunification is an extension of unification to first-order formulae over syntactic equality atoms. Instead of considering only syntactic equality, I extend a disunification algorithm by Comon and Delor to ultimately periodic interpretations, i.e.~minimal many-sorted Herbrand models of predicative Horn clauses and, for some sorts, equations of the form $s^\upmb(x)\eq s^\upma(x)$. The extended algorithm is terminating and correct for ultimately periodic interpretations over a finite signature and gives rise to a decision procedure for the satisfiability of equational formulae in ultimately periodic interpretations.

As an application, I show how to apply disunification to compute the completion of predicates with respect to an ultimately periodic interpretation. Such completions are a key ingredient to several inductionless induction methods.

URL for the Abstract:


Categories,
Keywords:


HyperLinks / References / URLs:


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:

@ARTICLE{HorbachWeidenbach2010,
AUTHOR = {Horbach, Matthias and Weidenbach, Christoph},
TITLE = {Superposition for Fixed Domains},
JOURNAL = {ACM Transactions on Computational Logic},
PUBLISHER = {ACM},
YEAR = {2010},
NUMBER = {4},
VOLUME = {11},
PAGES = {27,1--27,35},
ADDRESS = {New York, NY},
MONTH = {November},
ISBN = {1529-3785},
DOI = {10.1145/1805950.1805957},
}


Entry last modified by Anja Becker, 01/19/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
12/01/2010 10:50:37 AM
Revisions
2.
1.
0.

Editor(s)
Anja Becker
Matthias Horbach
Matthias Horbach

Edit Dates
19.01.2011 14:39:06
01.12.2010 10:57:02
01.12.2010 10:50:37

Show details for Attachment SectionAttachment Section
Hide details for Attachment SectionAttachment Section