A-sufficient substitutions in mixed contexts
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)
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.
Lecture Notes in Artificial Intelligence
Partial Inductive definitions, definiens computation, meta variables
Computer and Information Science
IdentifiersURN: urn:nbn:se:ri:diva-21195OAI: oai:DiVA.org:ri-21195DiVA: diva2:1041229
Proceedings of the Workshop Proof-Theoretic Extensions of Logic Programming at the International Conference on Logic Programming