Definitional Reflection and the Completion

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.

• Type: Conference
• Year: 1993
• Where: ELP
• Authors: Peter Schroeder-Heister
• Keywords: Automated Reasoning, Definitional Reflection, ELP 1993, Equality Theory, Free Equality