This is a formalization of Craig's interpolation theorem in propositional Classical Logic in Coq with Sequent Calculus using Maehara's method by induction on the length of proof tree.
TODO List (Future plans):
- Prove in intutionistic logic
- Cleaning the code
- Expand the proof to first order logic
- Expand the proof to Lyndon's Interpolation Theorem
- Prove using Pitts method
- Prove soundness and completeness of this Calculus over the traditional one (I might need to change the Bot rule and make some small changes to the proof so the context be finite)
- Prove Uniform Interpolation Theorem in Subsequent Logic