Mechanizing induction reasoning for first-order logic with inductive definitions
Sorin Stratulat, University of Lorraine, Metz, France
Abstract. Cyclic and explicit induction are two different reasoning techniques adapted to build proofs in the setting of classical first-order logic with inductive definitions. It has been shown that every explicit induction proof developed with the LKID inference system can be converted to a cyclic proof developed with the CLKIDω inference system. On the other hand, it has been proved recently that the conversion in the opposite direction is sometimes impossible.
We identify a class of proofs developed with a restricted version of CLKIDω that can be transformed into explicit induction proofs. The explicit induction proofs are built by following paths in the cyclic proofs which makes the transformation procedure easily automatisable. In practice, the transformation procedure can be at the core of an effective solution to implement cyclic induction reasoning by the current explicit induction-based first-order theorem provers.
The current approach for verifying the soundness of CLKIDω proofs is based on expensive model-checking techniques leading to an explosion in the number of states. We propose proof strategies that guarantee the soundness of CLKIDω proofs if some ordering constraints are satisfied. They are inspired from previous works about cyclic well- founded induction reasoning, known to provide effective sets of ordering constraints. In our case, an ordering constraint compares two sequents and can be decided in polynomial time in the size of the sequents. Under certain conditions, these strategies can help to build automatically proofs that implicitly satisfy the ordering constraints.