Computing Witnesses Using the SCAN Algorithm

Fabian Achammer, Stefan Hetzl, Renate A. Schmidt

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 no…