Computational Issues in Calculi of Partial Inductive Definitions

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 ofthis idea. Theories of partial inductive definitions (PID) constitute...

Full description

Bibliographic Details
Main Author: Kreuger, Per
Format: Doctoral Thesis
Language:English
Published: Decisions, Networks and Analytics lab 1995
Subjects:
Online Access:http://urn.kb.se/resolve?urn=urn:nbn:se:ri:diva-21196
id ndltd-UPSALLA1-oai-DiVA.org-ri-21196
record_format oai_dc
spelling ndltd-UPSALLA1-oai-DiVA.org-ri-211962017-10-13T05:15:52ZComputational Issues in Calculi of Partial Inductive DefinitionsengKreuger, PerDecisions, Networks and Analytics lab1995Theory of computationalgorithmslogicproof-theorypartial inductive defi-nitionsdefinitional reflectiondisunificationclosurecompletionnegationconstructive negationquantificationlogic programmingmeta programmingquantificationskolemizationself-referenceprogram semanticsdeclarative controlproof-searchtheorem-proving.Computer and Information ScienceData- och informationsvetenskapWe 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 ofthis 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 analyzethe 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 modelling tool GCLA II in which many of the computational prob-lems discussed arise naturally in practice. <p>Also published as SICS Dissertation no. SICS-D-19</p>Doctoral thesis, monographinfo:eu-repo/semantics/doctoralThesistexthttp://urn.kb.se/resolve?urn=urn:nbn:se:ri:diva-21196SICS dissertation series, 1101-1335 ; SICS-D-19application/postscriptinfo:eu-repo/semantics/openAccess
collection NDLTD
language English
format Doctoral Thesis
sources NDLTD
topic Theory of computation
algorithms
logic
proof-theory
partial inductive defi-nitions
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.
Computer and Information Science
Data- och informationsvetenskap
spellingShingle Theory of computation
algorithms
logic
proof-theory
partial inductive defi-nitions
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.
Computer and Information Science
Data- och informationsvetenskap
Kreuger, Per
Computational Issues in Calculi of Partial Inductive Definitions
description 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 ofthis 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 analyzethe 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 modelling tool GCLA II in which many of the computational prob-lems discussed arise naturally in practice. === <p>Also published as SICS Dissertation no. SICS-D-19</p>
author Kreuger, Per
author_facet Kreuger, Per
author_sort Kreuger, Per
title Computational Issues in Calculi of Partial Inductive Definitions
title_short Computational Issues in Calculi of Partial Inductive Definitions
title_full Computational Issues in Calculi of Partial Inductive Definitions
title_fullStr Computational Issues in Calculi of Partial Inductive Definitions
title_full_unstemmed Computational Issues in Calculi of Partial Inductive Definitions
title_sort computational issues in calculi of partial inductive definitions
publisher Decisions, Networks and Analytics lab
publishDate 1995
url http://urn.kb.se/resolve?urn=urn:nbn:se:ri:diva-21196
work_keys_str_mv AT kreugerper computationalissuesincalculiofpartialinductivedefinitions
_version_ 1718553568794902528