Max-Planck-Institut für Informatik
max planck institut
mpii logo Minerva of the Max Planck Society

MPI-INF RG1 Publications :: Thesis :: Horbach, Matthias

MPI-INF RG1 Publications
Show all entries of:this year (2019)last year (2018)two years ago (2017)Open in Notes
Action:login to update  Library locked

Thesis - Doctoral dissertation | @PhdThesis | Doktorarbeit

Author(s)*:Horbach, Matthias
BibTeX citekey*:Horbach2010PhD

Title, School
Title*:Superposition-based Decision Procedures for Fixed Domain and Minimal Model Semantics
School:Universität des Saarlandes
Type of Thesis*:Doctoral dissertation

Publishers Name:Universität des Saarlandes
Publishers Address:Saarbrücken

Note, Abstract, Copyright
LaTeX Abstract:Superposition is an established decision procedure for a variety of first-order logic theories represented by sets of clauses. A satisfiable theory, saturated by superposition, implicitly defines a minimal Herbrand model for the theory. This raises the question in how far superposition calculi can be employed for reasoning about such minimal models. This is indeed often possible when existential properties are considered. However, proving universal properties directly leads to a modification of the minimal model's term-generated domain, as new Skolem functions are introduced. For many applications, this is not desired because it changes the problem.

In this thesis, I propose the first superposition calculus that can explicitly represent existentially quantified variables and can thus compute with respect to a given fixed domain. It does not eliminate existential variables by Skolemization, but handles them using additional constraints with which each clause is annotated. This calculus is sound and refutationally complete in the limit for a fixed domain semantics. For saturated Horn theories and classes of positive formulas, the calculus is even complete for proving properties of the minimal model itself, going beyond the scope of known superposition-based approaches.

The calculus is applicable to every set of clauses with equality and does not rely on any syntactic restrictions of the input. Extensions of the calculus lead to various new decision procedures for minimal model validity. A main feature of these decision procedures is that even the validity of queries containing one quantifier alternation can be decided. In particular, I prove that the validity of any formula with at most one quantifier alternation is decidable in models represented by a finite set of atoms and that the validity of several classes of such formulas is decidable in models represented by so-called disjunctions of implicit generalizations. Moreover, I show that the decision of minimal model validity can be reduced to the superposition-based decision of first-order validity for models of a class of predicative Horn clauses where all function symbols are at most unary.

Download Access Level:Public
Download File(s):

Referees, Status, Dates
1. Referee:Christoph Weidenbach
2. Referee:Deepak Kapur
Supervisor:Christoph Weidenbach
Date Kolloquium:22 July 2010
Chair Kolloquium:Markus Bläser

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:
AUTHOR = {Horbach, Matthias},
TITLE = {Superposition-based Decision Procedures for Fixed Domain and Minimal Model Semantics},
PUBLISHER = {Universität des Saarlandes},
SCHOOL = {Universit{\"a}t des Saarlandes},
YEAR = {2010},
TYPE = {Doctoral dissertation}
PAGES = {186},
ADDRESS = {Saarbr{\"u}cken},
MONTH = {July},

Entry last modified by Anja Becker, 02/07/2011
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)

12/01/2010 11:01:32 AM

Anja Becker
Matthias Horbach

Edit Date
07.02.2011 13:09:55
01.12.2010 11:01:32