A Non-Binary Method for Finding Interpolants: Theory and Practice
This work addresses a specific problem in formal logic and proof theory, offering an incremental improvement over existing interpolant-searching methods.
The paper tackles the problem of finding interpolants in classical logic by introducing a new method based on a non-binary version of resolution, resulting in a novel approach that leverages refutation systems as a starting point.
We describe a new method of finding interpolants for classical logic using certain refutation system as a starting point. Refutation can be thought of as an alternative approach to the analysis of formal systems: instead of focusing on which formulas provably belong to a given logic, it shows which formulas are to be rejected. Thus, it provides a mirror proof system. As it turns out, the benefits of such an approach go well beyond the area of refutation calculi themselves. We provide one such example in the shape of an interpolant-searching method. To be sure, a number of such methods are already in use. The novelty of our proposal lies in the fact that it can be considered as based on a non-binary version of resolution.