Second-Order Quantified Boolean Logic


  • Jie-Hong R. Jiang National Taiwan University



CSO: Other Foundations of Constraint Satisfaction & Optimization, CSO: Constraint Satisfaction, CSO: Satisfiability, KRR: Automated Reasoning and Theorem Proving, KRR: Computational Complexity of Reasoning, KRR: Other Foundations of Knowledge Representation & Reasoning


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.




How to Cite

Jiang, J.-H. R. (2023). Second-Order Quantified Boolean Logic. Proceedings of the AAAI Conference on Artificial Intelligence, 37(4), 4007-4015.



AAAI Technical Track on Constraint Satisfaction and Optimization