Computing Witnesses Using the SCAN Algorithm
For researchers in computational logic, this is an incremental extension of an existing algorithm to a related problem.
The paper extends the SCAN algorithm for second-order quantifier elimination to also compute witnesses for the second-order quantifiers, and provides a prototype implementation.
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.