Change search
ReferencesLink to record
Permanent link

Direct link
A-sufficient substitutions in mixed contexts
RISE, Swedish ICT, SICS. IAM.
Number of Authors: 1
1994 (English)In: Proceedings of the Workshop Proof-Theoretic Extensions of Logic Programming at the International Conference on Logic Programming, Springer LNAI Extensions of Logic Programming at the International Conference on Logic Programming, 1994, 1, Vol. 596, 6 p.38-43 p.Conference paper (Refereed)
Abstract [en]

In proof-systems based on calculi of Partial Inductive Definitions (PID), the notion of an A-sufficient substitution is of central importance. Applying an A-sufficient substitution to an atom before computing its definiens is necessary for the rule of definitional reflection to be sound. So far computation of A-sufficient substitutions have been restricted to the case where all variables in a query (sequent to be proved) are existentially quantified, i.e. logical variables in the sense of Prolog. From a proof theoretic point of view this kind of variable can be regarded as metavariables i.e. place-holders for as yet unknown terms. In a finitary calculus of PID's these eigenvariables have to be bound by the rule of definitional reflection in order to preserve soundness (with respect to an underlying infinitary system of PID's). This property makes these calculi different from most (if not all) calculi based on more traditional logics. This note explores some computational issues in connectin with such caluculi.

Place, publisher, year, edition, pages
1994, 1. Vol. 596, 6 p.38-43 p.
Series
, Lecture Notes in Artificial Intelligence
Keyword [en]
Partial Inductive definitions, definiens computation, meta variables
National Category
Computer and Information Science
Identifiers
URN: urn:nbn:se:ri:diva-21195OAI: oai:DiVA.org:ri-21195DiVA: diva2:1041229
Conference
Proceedings of the Workshop Proof-Theoretic Extensions of Logic Programming at the International Conference on Logic Programming
Note
LNAI, SpringerAvailable from: 2016-10-31 Created: 2016-10-31

Open Access in DiVA

fulltext(102 kB)0 downloads
File information
File name FULLTEXT01.psFile size 102 kBChecksum SHA-512
774c5ea7f61510a0b693c2821cca7c29f4f3ade1413bc3d35d724d11b6d55642fb4e3e869431bfd6950d690f1c8c52d2cedfa1cd9f5f3ebb19a399bf4a26610a
Type fulltextMimetype application/postscript

By organisation
SICS
Computer and Information Science

Search outside of DiVA

GoogleGoogle Scholar
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

ReferencesLink to record
Permanent link

Direct link