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

Publications Master Template :: Thesis :: Stuber, Jürgen

Publications Master Template
Show all entries of:this year (2020)last year (2019)two years ago (2018)Open in Notes
Action:login to update

Thesis - Master's thesis | @MastersThesis | Masterarbeit

Author(s)*:Stuber, Jürgen
BibTeX citekey*:Stuber91

Title, School
Title*:Inductive Theorem Proving for {H}orn Clauses
School:Universität Dortmund
Type of Thesis*:Master's thesis

Note, Abstract, Copyright
LaTeX Abstract:We show how to prove inductive consequences of horn clause specifications by horn clause completion. Most often one is interested in properties of the initial algebra. These stem from the facts that (a) it is generated by ground terms, and that (b) only provable ground equations are valid in the initial algebra. (a) is the basis of proofs by structural induction. (b) becomes relevant in the case of horn clauses, since the validity of a horn clause may depend on the fact that the conditions do not become true too often. We show that (a) is true for term generated algebras, whereas (b) is true for free algebras. Sophisticated completion procedures for horn clauses already carry out inductive proofs of type (b), in order to

avoid orienting rules whose conditions are false in the resulting
conditional rewrite system. To apply this to properties of type (a),
we transform the specification, expressing the fact that a term t is
ground as the provability of an atom gnd(t). By choosing a suitable
selection strategy, we obtain proof procedures for the initial model,
the class of all term generated models and the class of all free models.
Additionally, it is possible to prove sufficient completeness of a
specification. All our proof procedures are refutationally complete
and linear.

Download Access Level:Public
Download File(s):View attachments here:

Referees, Status, Dates
Date Kolloquium:23 March 1998

MPG Unit:Max-Planck-Institut für Informatik
MPG Subunit:Programming Logics Group
Appearance:MPII WWW Server

BibTeX Entry:
AUTHOR = {Stuber, J{\"u}rgen},
TITLE = {Inductive Theorem Proving for {H}orn Clauses},
SCHOOL = {Universit{\"a}t Dortmund},
YEAR = {1991},
TYPE = {Master's thesis}

Hide details for Attachment SectionAttachment Section

View attachments here:

Entry last modified by Uwe Brahm, 03/12/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)

Uwe Brahm
03/23/1998 07:50:43 PM
Uwe Brahm
Uwe Brahm
Uwe Brahm
Christine Kiesel
Christine Kiesel
Edit Dates
2007-07-02 11:11:03
2007-07-02 11:10:39
2007-07-02 10:56:07
14.09.2001 03:30:22 PM
03/23/98 07:54:35 PM