Computing Witnesses Using the SCAN Algorithm

TL;DR

This paper extends the SCAN algorithm to compute witnesses for second-order quantifiers, enabling the derivation of equivalent first-order formulas, with a prototype implementation demonstrating its practical application.

Contribution

The paper introduces an extension of the SCAN algorithm to find witnesses for second-order quantifiers, broadening its applicability in computational logic.

Findings

Extended SCAN algorithm can find witnesses for second-order quantifiers.

Prototype implementation demonstrates practical feasibility.

Method produces logically equivalent first-order formulas.

Abstract

Second-order quantifier elimination is the problem of finding, given a formula with second-order quantifiers, a logically equivalent first-order formula. While such formulas are not computable in general, there are practical algorithms and subclasses with applications throughout computational logic. One of the most prominent algorithms for second-order quantifier elimination is the saturation-based SCAN algorithm. In this paper we show how the SCAN algorithm on clause sets can be extended to solve a more general problem: namely, finding a witness for the second-order quantifiers that results in a logically equivalent first-order formula. In addition, we provide a prototype implementation of the proposed method.