Finitary Partial Inductive Definitions as a General Logic

We describe how the calculus of partial inductive definitions is used to represent logics. This calculus includes the powerful principle of definitional reflection. We describe two conceptually different approaches to representing a logic, both making essential use of definitional reflection. In the deductive approach, the logic is defined by its inference rules. Only the succedent rules (in a sequent calculus

• Type: Conference
• Year: 1993
• Where: ELP
• Authors: Lars-Henrik Eriksson
• Keywords: Automated Reasoning, Calculus, Definitional Reflection, ELP 1993, Partial Inductive Definitions