The logic of definitional reflection is extended with a theory of free equality. Based on this equality theory a sequent-style notion of the completion of a definition is motivated. Definitional reflection with free equality turns out to be equivalent to the completion in this sense.
CITATION STYLE
Schroeder-Heister, P. (1994). Definitional reflection and the completion. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 798 LNAI, pp. 322–347). Springer Verlag. https://doi.org/10.1007/3-540-58025-5_65
Mendeley helps you to discover research relevant for your work.