Second-Order Quantified Boolean Logic

@article{Jiang_2023, title={Second-Order Quantified Boolean Logic}, volume={37}, url={https://ojs.aaai.org/index.php/AAAI/article/view/25515}, DOI={10.1609/aaai.v37i4.25515}, abstractNote={Second-order quantified Boolean formulas (SOQBFs) generalize quantified Boolean formulas (QBFs) by admitting second-order quantifiers on function variables in addition to first-order quantifiers on atomic variables. Recent endeavors establish that the complexity of SOQBF satisfiability corresponds to the exponential-time hierarchy (EXPH), similar to that of QBF satisfiability corresponding to the polynomial-time hierarchy (PH). This fact reveals the succinct expression power of SOQBFs in encoding decision problems not efficiently doable by QBFs. In this paper, we investigate the second-order quantified Boolean logic with the following main results: First, we present a procedure of quantifier elimination converting SOQBFs to QBFs and a game interpretation of SOQBF semantics. Second, we devise a sound and complete refutation-proof system for SOQBF. Third, we develop an algorithm for countermodel extraction from a refutation proof. Finally, we show potential applications of SOQBFs in system design and multi-agent planning. With these advances, we anticipate practical tools for development.}, number={4}, journal={Proceedings of the AAAI Conference on Artificial Intelligence}, author={Jiang, Jie-Hong R.}, year={2023}, month={Jun.}, pages={4007-4015} }