Computing Witnesses Using the SCAN Algorithm
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.
Cite
@article{arxiv.2604.27939,
title = {Computing Witnesses Using the SCAN Algorithm},
author = {Fabian Achammer and Stefan Hetzl and Renate A. Schmidt},
journal= {arXiv preprint arXiv:2604.27939},
year = {2026}
}
Comments
submitted to Journal of Automated Reasoning (Selected Extended Papers of CADE 2025); 62 pages. arXiv admin note: text overlap with arXiv:2506.00163