Proceedings Article, Paper
@InProceedings
Beitrag in Tagungsband, Workshop


Show entries of:

this year (2019) | last year (2018) | two years ago (2017) | Notes URL

Action:

login to update

Options:








Author, Editor

Author(s):

Kruglov, Evgeny
Weidenbach, Christoph

dblp
dblp



Editor(s):

Ratschan, Stefan

dblp

Not MPII Editor(s):

Ratschan, Stefan

BibTeX cite key*:

KruglovMACIS2011

Title, Booktitle

Title*:

SUP(T) Decides First-Order Logic Fragment Over Ground Theories

Booktitle*:

Fourth International Conference on Mathematical Aspects of Computer and Information Sciences (MACIS-4)

Event, URLs

URL of the conference:

http://macis2011.cc4cm.org

URL for downloading the paper:


Event Address*:

Beijing, China

Language:

English

Event Date*
(no longer used):


Organization:


Event Start Date:

19 October 2011

Event End Date:

21 October 2011

Publisher

Name*:

Internal Conference Proceedings

URL:


Address*:

Beijing, China

Type:


Vol, No, Year, pp.

Series:


Volume:


Number:


Month:


Pages:


Year*:

2011

VG Wort Pages:


ISBN/ISSN:


Sequence Number:


DOI:




Note, Abstract, ©


(LaTeX) Abstract:

The hierarchic superposition calculus 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) is terminating for the transformed clause set, hence 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.

Keywords:

Theorem proving, combination of theories, decision procedure, arithmetic



Download
Access Level:

Public

Correlation

MPG Unit:

Max-Planck-Institut für Informatik



MPG Subunit:

Automation of Logic

Audience:

experts only

Appearance:

MPII WWW Server, MPII FTP Server, MPG publications list, university publications list, working group publication list, Fachbeirat, VG Wort



BibTeX Entry:

@INPROCEEDINGS{KruglovMACIS2011,
AUTHOR = {Kruglov, Evgeny and Weidenbach, Christoph},
EDITOR = {Ratschan, Stefan},
TITLE = {{SUP(T)} Decides First-Order Logic Fragment Over Ground Theories},
BOOKTITLE = {Fourth International Conference on Mathematical Aspects of Computer and Information Sciences (MACIS-4)},
PUBLISHER = {Internal Conference Proceedings},
YEAR = {2011},
ADDRESS = {Beijing, China},
}


Entry last modified by Evgeny Kruglov, 06/08/2012
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)
Evgeny Kruglov
Created
06/08/2012 02:11:32 PM
Revision
0.



Editor
Evgeny Kruglov



Edit Date
06/08/2012 02:11:32 PM



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