Logic in Computer Science (LICS 1993)

Paper: Rules of definitional reflection (at LICS 1993)

Authors: Peter Schroeder-Heister

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

BibTeX

  @InProceedings{SchroederHeister-Rulesofdefinitional,
    author = 	 {Peter Schroeder-Heister},
    title = 	 {Rules of definitional reflection},
    booktitle =  {Proceedings of the Eighth Annual IEEE Symp. on Logic in Computer Science, {LICS} 1993},
    year =	 1993,
    editor =	 {Moshe Vardi},
    month =	 {June}, 
    pages =      {222--232},
    location =   {Montreal, Canada}, 
    publisher =	 {IEEE Computer Society Press}
  }