Second-Order Quantified Boolean Logic

Authors: Jie-Hong R. Jiang

AAAI 2023 | Conference PDF | Archive PDF | Plain Text | LLM Run Details

Reproducibility Variable Result LLM Response
Research Type Theoretical 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.
Researcher Affiliation Academia Jie-Hong R. Jiang Graduate Institute of Electronics Engineering, National Taiwan University, Taipei, Taiwan Department of Electrical Engineering, National Taiwan University, Taipei, Taiwan jhjiang@ntu.edu.tw
Pseudocode Yes Algorithm 1: Countermodel Extraction
Open Source Code No The paper does not provide any explicit statements about releasing source code for the described methodology, nor does it include links to a code repository.
Open Datasets No The paper is theoretical and does not conduct empirical studies using datasets for training, validation, or testing. The examples provided (Example 1, Example 2) are illustrative within the theoretical framework.
Dataset Splits No The paper is theoretical and does not conduct empirical studies. Therefore, it does not specify dataset splits for validation or other purposes.
Hardware Specification No The paper is theoretical and does not describe any empirical experiments that would require specific hardware. No hardware specifications are mentioned.
Software Dependencies No The paper is theoretical and does not describe any empirical experiments or implementations that would require specific software dependencies with version numbers.
Experiment Setup No The paper is theoretical and does not describe any empirical experiments or their setup, hyperparameters, or training configurations.