Rules of definitional reflection

Author

Schroeder-Heister, Peter

Author_Institution

Wilhelm-Schickard-Inst. fur Inf., Tubingen Univ., Germany

fYear

1993

fDate

19-23 Jun 1993

Firstpage

222

Lastpage

232

Abstract

The author discusses two rules of definitional reflection: the logical version of definitional reflection, as used in the extended logic programming language GCLA, and the ω version of definitional reflection. The logical version 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 interpretation of free variables differs between the two approaches, resulting in different principles of closure of inference rules under substitution. This difference is crucial for the computational interpretation of definitional reflection

Keywords

formal logic; inference mechanisms; logic programming; logic programming languages; programming theory; GCLA; Gentzen-style sequent systems; arithmetic; computational interpretation; definitional reflection rules; extended logic programming language; first order logic; inference rules; left-introduction rule; logical operators; logical version; omega version; substitution; Arithmetic; Calculus; Databases; History; Logic programming; Reflection;

fLanguage

English

Publisher

ieee

Conference_Titel

Logic in Computer Science, 1993. LICS '93., Proceedings of Eighth Annual IEEE Symposium on

Conference_Location

Montreal, Que.

Print_ISBN

0-8186-3140-6

Type

conf

DOI

10.1109/LICS.1993.287585

Filename

287585