Second-Order Quantified Boolean Logic
Abstract
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.
Cite
Text
Jiang. "Second-Order Quantified Boolean Logic." AAAI Conference on Artificial Intelligence, 2023. doi:10.1609/AAAI.V37I4.25515Markdown
[Jiang. "Second-Order Quantified Boolean Logic." AAAI Conference on Artificial Intelligence, 2023.](https://mlanthology.org/aaai/2023/jiang2023aaai-second/) doi:10.1609/AAAI.V37I4.25515BibTeX
@inproceedings{jiang2023aaai-second,
title = {{Second-Order Quantified Boolean Logic}},
author = {Jiang, Jie-Hong R.},
booktitle = {AAAI Conference on Artificial Intelligence},
year = {2023},
pages = {4007-4015},
doi = {10.1609/AAAI.V37I4.25515},
url = {https://mlanthology.org/aaai/2023/jiang2023aaai-second/}
}