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):

Kruglov, Evgeny
Weidenbach, Christoph

dblp
dblp



BibTeX cite key*:

KruglovWeidenbachMCS2012

Title

Title*:

Superposition Decides the First-Order Logic Fragment Over Ground Theories

Journal

Journal Title*:

Mathematics in Computer Science

Journal's URL:

http://link.springer.com/journal/11786

Download URL
for the article:

http://link.springer.com/content/pdf/10.1007%2Fs11786-012-0135-4

Language:

English

Publisher

Publisher's
Name:

Birkhäuser

Publisher's URL:

http://www.springer.com/birkhauser

Publisher's
Address:

Basel

ISSN:

1661-8270

Vol, No, pp, Date

Volume*:

6

Number:

4

Publishing Date:

December 2012

Pages*:

427-456

Number of
VG Pages:


Page Start:

427

Page End:

456

Sequence Number:


DOI:

10.1007/s11786-012-0135-4

Note, Abstract, ©

Note:


(LaTeX) Abstract:

The hierarchic superposition calculus over a theory T, called SUP(T), enables sound reasoning on the hierarchic combination
of a theory T with full first-order logic, FOL(T). If a FOL(T) clause set enjoys a sufficient completeness criterion,
the calculus is even complete. Clause sets over the ground fragment of FOL(T) are not sufficiently complete, in general.
In this paper we show that any clause set over the ground FOL(T) fragment can be transformed into a sufficiently complete one,
and prove that SUP(T) terminates on the transformed clause set, hence constitutes a decision procedure provided the
existential fragment of the theory T is decidable. Thanks to the hierarchic design of SUP(T), the decidability result
can be extended beyond the ground case. We show SUP(T) is a decision procedure for the non-ground FOL fragment
plus a theory T, if every non-constant function symbol from the underlying FOL signature ranges into the sort of the theory T,
and every term of the theory sort is ground. Examples for T are in particular decidable fragments of arithmetic.

URL for the Abstract:


Categories,
Keywords:

Theorem proving, Combination of theories, Decision procedure, Arithmetic

HyperLinks / References / URLs:


Copyright Message:


Personal Comments:


Download
Access Level:

Internal

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{KruglovWeidenbachMCS2012,
AUTHOR = {Kruglov, Evgeny and Weidenbach, Christoph},
TITLE = {Superposition Decides the First-Order Logic Fragment Over Ground Theories},
JOURNAL = {Mathematics in Computer Science},
PUBLISHER = {Birkhäuser},
YEAR = {2012},
NUMBER = {4},
VOLUME = {6},
PAGES = {427--456},
ADDRESS = {Basel},
MONTH = {December},
ISBN = {1661-8270},
DOI = {10.1007/s11786-012-0135-4},
}


Entry last modified by Anja Becker, 03/07/2013
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
02/13/2013 07:06:51 PM
Revision
1.
0.


Editor
Anja Becker
Evgeny Kruglov


Edit Date
07.03.2013 13:56:33
02/13/2013 07:06:51 PM