A-sufficient substitutions in mixed contexts

Kreuger, Per (1994) A-sufficient substitutions in mixed contexts. In: Proceedings of the Workshop Proof-Theoretic Extensions of Logic Programming at the International Conference on Logic Programming, 1994, Santa Margherita Ligure.



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.

Item Type:Conference or Workshop Item (Paper)
Additional Information:LNAI, Springer
Uncontrolled Keywords:Partial Inductive definitions, definiens computation, meta variables
ID Code:576
Deposited By:IAM Researcher
Deposited On:03 Apr 2009
Last Modified:18 Nov 2009 15:57

Repository Staff Only: item control page