A Non-Binary Method for Finding Interpolants: Theory and Practice

TL;DR

This paper introduces a novel non-binary resolution-based method for finding interpolants in classical logic, leveraging refutation systems to enhance the analysis of formal systems and improve interpolant search techniques.

Contribution

It presents a new non-binary resolution approach for interpolant generation, expanding the theoretical framework and practical methods beyond existing binary resolution techniques.

Findings

Demonstrates the effectiveness of the non-binary interpolant search method.

Provides theoretical foundations linking refutation systems and interpolant computation.

Shows practical advantages over traditional binary resolution methods.

Abstract

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.