Fully declarative programming with logic mathematical foundations.
Item
-
Title
-
Fully declarative programming with logic mathematical foundations.
-
Identifier
-
AAI9108165
-
identifier
-
9108165
-
Creator
-
Plaza, Jan Andrzej.
-
Contributor
-
Adviser: Melvin Fitting
-
Date
-
1990
-
Language
-
English
-
Publisher
-
City University of New York.
-
Subject
-
Computer Science | Mathematics
-
Abstract
-
Great hope for programming correctness has been centered in logic programming because of its declarativeness, but the declarativeness depends on the technical condition of completeness: solutions computed by resolution should be exactly the logical consequences of an easily understandable completion of the program. For resolutions allowing negation {dollar}\neg{dollar}, such as SLDNF-resolution or Prolog's resolution, this goal has not been yet achieved, even for propositional programs.;In this paper we consider programs involving {dollar}\neg{dollar}, {dollar}\forall{dollar}, {dollar}\exists{dollar} and =. At the propositional level we prove completeness of SLDNF-resolution for the full class of programs with {dollar}\neg{dollar} (including normal programs). This is done in several ways in classical, intuitionistic, intermediate and in modal logics. We use intuitively natural notions of constructive completions of programs. These results can be of importance for expert systems. At the first-order level, we formulate resolution systems extending SLD-resolution, but alternative to SLDNF. We prove their completeness for the full class of positive programs (involving {dollar}\forall{dollar}, {dollar}\exists{dollar}, =), and also for some classes of programs involving negative information. This guarantees declarativeness of logic programming for a wide variety of programs. Examples suggest that extending completeness (declarativeness) further, is not possible because of certain inherent properties of these wider classes of programs.;Several techniques of this paper, connected with an alterative notion of a Herbrand model, least fix-points of operators, and decidability of an equality theory that extends Clark's theory, may be applicable in other problems from the theory of logic programming.
-
Type
-
dissertation
-
Source
-
PQT Legacy CUNY.xlsx
-
degree
-
Ph.D.
