Continuing my research into classical algorithms for working with logics, I ported propositional interpolation from Isabelle to SSReflect: craig_interp.v.
The interpolation property was introduced by William Craig in 1957 - a logical system has it if, for any two formulas A and B, such that the validity of the latter follows from the validity of the former, it is possible to find an “intermediate” formula I whose validity follows from the validity of A and entails the validity of B; at the same time, all variables in it occur in both original formulas (i.e., in general one cannot just take A or B as I). This property was further shown for many logics - propositional, first-order, a number of modal and multi-sorted ones, etc., often by constructive methods, which allows us to realize the procedure of finding I as an algorithm. Later, a number of results on the complexity of the interpolation procedure were also obtained, in particular the connection with the P=NP problem. In the 2000s, McMillan proposed the use of interpolation to quickly approximate invariants in SAT-solving based model checkers. For more details, see the slides in D’Silva, [2016] “Interpolation: Theory and Applications”.