We're sorry but this page doesn't work properly without JavaScript enabled. Please enable it to continue.
Feedback

The Symmetry Rule for Quantified Boolean Formulas

Formal Metadata

Title
The Symmetry Rule for Quantified Boolean Formulas
Title of Series
Number of Parts
28
Author
Contributors
License
CC Attribution - NonCommercial - NoDerivatives 4.0 International:
You are free to use, copy, distribute and transmit the work or content in unchanged form for any legal and non-commercial purpose as long as the work is attributed to the author in the manner specified by the author or licensor.
Identifiers
Publisher
Release Date
Language

Content Metadata

Subject Area
Genre
Abstract
One of the oldest and weakest calculi for quantified Boolean formulas (QBF) is Q-Resolution. It consists of two rules: the resolution rule similar as in propositional logic and the universal reduction rule. In its most basic variant, resolution is allowed only over existential variables. More powerful proof systems can be obtained by allowing resolution over the universal variables as well or by introducing so-called long-distance resolution. Separations are shown by using the well-investigated formulas introduced by Kleine Buening and other (the so-called KBKF formulas). In this talk, we enrich the (relatively weak) QBF resolution calculus with the Symmetry Rule that exploits symmetries of the input formula. With this simple rule, we obtain separations to powerful QBF calculi by showing that the KBKF formulas and extensions become easy when the symmetry rule may be used.