LPC(ID): A Sequent Calculus Proof System for Propositional Logic Extended with Inductive Definitions

Ping Hou, Johan Wittocx, Marc Denecker

The logic FO(ID) uses ideas from the field of logic programming to extend first order logic with non-monotone inductive definitions. Such logic formally extends logic programming,…