Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

Adam Trybus, Karolina Rożko, Tomasz Skura

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.

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

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.
Paper Structure (11 sections, 1 theorem, 7 equations, 3 figures)

This paper contains 11 sections, 1 theorem, 7 equations, 3 figures.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Syntax.
  4. Semantics.
  5. Previous work
  6. Refutation
  7. Theoretical results --- the interpolant-finding procedure
  8. Implementation
  9. The program
  10. Experimental results
  11. Conclusions

Key Result

Theorem 1

All formulas $X$ and $Y$ such that $\models X \to Y$ have an interpolant.

Figures (3)

  • Figure 1: Execution time [sec] ($y$ axis) and the size of $X \to Y$ ($x$ axis) for various experimental settings. Regression line in blue.
  • Figure 2: Execution time [sec] ($y$ axis) and the size of interpolant ($x$ axis). Regression line shown in blue.
  • Figure 3: Execution time [sec] and (a) the size of $X \to Y$ (b) the size of the interpolant. Regression lines in blue.

Theorems & Definitions (3)

  • Theorem : Extended Interpolation Theorem
  • proof
  • Example