A Sequent Calculus for General Inductive Definitions
This work provides a theoretically substantiated proof system for FO(ID), enabling formal proofs of theorems involving general inductive definitions, which is important for knowledge representation and reasoning.
The authors extend an existing sequent calculus LKID to SCFO(ID) for the logic FO(ID), which includes general non-monotone inductive definitions. They overcome the challenge of non-monotonicity by drawing inspiration from stable semantics, and establish proof-theoretical properties and demonstrate the calculus on examples.
Inductive definitions are an important form of knowledge. The logic FO(ID) is an extension of classical first-order logic FO with general non-monotone inductive definitions. Most existing proof systems for inductive definitions impose syntactic constraints on their definitions, thereby excluding many useful and natural definitions. We extend an existing sequent calculus LKID by Brotherston and Simpson, founded on the principle of mathematical induction, to a sequent calculus SCFO(ID) for FO(ID). The main challenge in this extension is the accommodation of non-monotone inductive definitions. To overcome this challenge, we draw inspiration from the stable semantics, which is a commonly used semantics in logic programming that is closely related to the well-founded semantics behind FO(ID). We corroborate SCFO(ID) by establishing several proof-theoretical properties and through demonstration on various examples. In conclusion, SCFO(ID) is a theoretically substantiated sequent calculus for FO(ID), enabling formal proofs of theorems involving general inductive definitions.