Rules of definitional reflection
- 31 December 2002
- proceedings article
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- p. 222-232
- https://doi.org/10.1109/lics.1993.287585
Abstract
This paper discusses two rules of definitional reflec- tion: The "logical" version of definitional reflection as used in the extended logic programming language GCLA and the "!"-version of definitional reflection as proposed by Eriksson and Girard. The logical ver- sion is a Left-introduction rule completely analogous to the Left-introduction rules for logical operators in Gentzen-style sequent systems, whereas the !-version extends the logical version by a principle related to the !-rule in arithmetic. Correspondingly, the inter- pretation of free variables differs between the two ap- proaches, resulting in different principles of closure of inference rules under substitution. This difference is crucial for the computational interpretation of defini- tional reflection.Keywords
This publication has 17 references indexed in Scilit:
- Logic programming, functional programming, and inductive definitionsPublished by Springer Nature ,2006
- A finitary version of the calculus of partial inductive definitionsPublished by Springer Nature ,2005
- An Intuitionistic Predicate Logic Theorem ProverJournal of Logic and Computation, 1992
- Partial inductive definitionsTheoretical Computer Science, 1991
- A Proof-Theoretic Approach to Logic Programming. I. Clauses as RulesJournal of Logic and Computation, 1990
- A natural extension of natural deductionThe Journal of Symbolic Logic, 1984
- Negation as FailurePublished by Springer Nature ,1978
- Hauptsatz for the Intuitionistic Theory of Iterated Inductive DefinitionsPublished by Elsevier ,1971
- Einführung in die Operative Logik und MathematikPublished by Springer Nature ,1955
- The inconsistency of certain formal logicsThe Journal of Symbolic Logic, 1942