#
Computational Issues in Calculi of Partial Inductive Definitions

### Abstract

*We study the properties of a number of algorithms proposed to explore the
computational space generated by a very simple and general idea: the notion of
a mathematical definition and a number of suggested formal interpretations of
this idea.*
*Theories of partial inductive definitions (PID) constitute a class of
logics based on the notion of an inductive definition. Formal systems based on
this notion can be used to generalize Horn-logic and naturally allow and
suggest extensions which differ in interesting ways from generalizations based
on first order predicate calculus. E.g. the notion of completion generated by
a calculus of PID and the resulting notion of negation is completely natural
and does not require externally motivated procedures such as "negation as
failure".*

*For this reason computational issues arising in these calculi deserve
closer inspection. This work discuss a number of finitary theories of PID and
analyze the algorithmic and semantical issues that arise in each of
them.*

*There has been significant work on implementing logic programming
languages in this setting and we briefly present the programming language and
knowledge modeling tool GCLAII in which many of the computational problems
discussed arise naturally in practice.*

## Descriptors:

Theory of computation, algorithms, logic, proof-theory, partial inductive
definitions, definitional reflection, disunification, closure, completion,
negation, constructive negation, quantification, logic programming, meta
programming, quantification, skolemization, self-reference, program semantics,
declarative control, proof-search, theorem-proving.
## The thesis is published as:

SICS Dissertation Series SICS-D--19.

Updated 00-09-08 by