Computing Witnesses Using the SCAN Algorithm (Extended Preprint)

TL;DR

This paper extends the SCAN algorithm, originally used for second-order quantifier elimination, to find specific instances of second-order quantifiers that produce equivalent first-order formulas, with a prototype implementation demonstrating its potential.

Contribution

The paper introduces an extension of the SCAN algorithm to solve a more general problem of finding quantifier instances, enabling broader applications in logic and verification.

Findings

Extended SCAN algorithm for quantifier instance finding

Prototype implementation demonstrating practical feasibility

Potential applications in modal logic, knowledge representation, and verification

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 SCAN algorithm which is based on saturation theorem proving. In this paper we show how the SCAN algorithm on clause sets can be extended to solve a more general problem: namely, finding an instance of the second-order quantifiers that results in a logically equivalent first-order formula. In addition we provide a prototype implementation of the proposed method. This work paves the way for applying the SCAN algorithm to new problems in application domains such as modal correspondence theory, knowledge representation, and verification.