MPI-INF Logo
Publications

Server    domino.mpi-inf.mpg.de

Proceedings Article, Paper
@InProceedings
Beitrag in Tagungsband, Workshop

Author, Editor
Author(s):
Horbach, Matthias
Weidenbach, Christoph
dblp
dblp
Editor(s):
Schmidt, Renate A.dblp
Not MPII Editor(s):
Schmidt, Renate A.
BibTeX cite key*:
HorbachWeidenbach2009CADE
Title, Booktitle
Title*:
Decidability Results for Saturation-Based Model Building
Booktitle*:
Automated Deduction - CADE-22 : 22nd International Conference on Automated Deduction
Event, URLs
Conference URL::
http://complogic.cs.mcgill.ca/cade22/
Downloading URL:
http://dx.doi.org/0.1007/978-3-642-02959-2_30
Event Address*:
Montreal, Canada
Language:
English
Event Date*
(no longer used):
Organization:
Event Start Date:
2 August 2009
Event End Date:
7 August 2009
Publisher
Name*:
Springer
URL:
http://www.springer.de/
Address*:
Berlin, Germany
Type:
Vol, No, Year, pp.
Series:
Lecture Notes in Artificial Intelligence
Volume:
5663
Number:
Month:
Pages:
404-420
Year*:
2009
VG Wort Pages:
ISBN/ISSN:
978-3-642-02958-5
Sequence Number:
DOI:
0.1007/978-3-642-02959-2_30
Note, Abstract, ©
(LaTeX) Abstract:
Saturation-based calculi such as superposition can be successfully instantiated to decision procedures for many decidable fragments of first-order logic. In case of termination without generating an empty clause, a saturated clause set implicitly represents a minimal model for all clauses, based on the underlying term ordering of the superposition calculus. In general, it is not decidable whether a ground atom, a clause or even a formula holds in this minimal model of a satisfiable saturated clause set.

We extend our superposition calculus for fixed domains with syntactic disequality constraints in a non-equational setting. Based on this calculus, we present several new decidability results for validity in the minimal model of a satisfiable finitely saturated clause set that in particular extend the decidability results known for ARM (Atomic Representations of term Models) and DIG (Disjunctions of Implicit Generalizations) model representations.
Keywords:
Decidability, Ordered Resolution, Model Building
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:

@INPROCEEDINGS{HorbachWeidenbach2009CADE,
AUTHOR = {Horbach, Matthias and Weidenbach, Christoph},
EDITOR = {Schmidt, Renate A.},
TITLE = {Decidability Results for Saturation-Based Model Building},
BOOKTITLE = {Automated Deduction - CADE-22 : 22nd International Conference on Automated Deduction},
PUBLISHER = {Springer},
YEAR = {2009},
VOLUME = {5663},
PAGES = {404--420},
SERIES = {Lecture Notes in Artificial Intelligence},
ADDRESS = {Montreal, Canada},
ISBN = {978-3-642-02958-5},
DOI = {0.1007/978-3-642-02959-2_30},
}


Entry last modified by Anja Becker, 03/25/2010
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
04/24/2009 11:58:29 AM
Revisions
6.
5.
4.
3.
2.
Editor(s)
Anja Becker
Jennifer Müller
Jennifer Müller
Jennifer Müller
Jennifer Müller
Edit Dates
25.03.2010 11:30:45
23.10.2009 15:24:03
23.10.2009 15:22:45
23.10.2009 15:22:37
23.10.2009 15:20:06