MPI-INF Logo
Publications

Server    domino.mpi-inf.mpg.de

Proceedings Article, Paper
@InProceedings
Beitrag in Tagungsband, Workshop

Author, Editor
Author(s):
Kruglov, Evgeny
Weidenbach, Christoph
dblp
dblp
Editor(s):
Ratschan, Stefandblp
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
Conference URL::
http://macis2011.cc4cm.org
Downloading URL:
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
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