Title	The Symmetry Rule for Quantified Boolean Formulas
Creator	Seidl, Martina
Publisher	Banff International Research Station for Mathematical Innovation and Discovery
Date Issued	2018-08-30T16:35
Description	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.
Extent	26.0
Subject	Mathematics; Computer science; Mathematical logic and foundations; Theoretical computer science
Type	Moving Image
File Format	video/mp4
Language	eng
Notes	Author affiliation: Johannes Kepler University
Series	BIRS Workshop Lecture Videos (Oaxaca de Juárez (Mexico))
Date Available	2019-04-05
Provider	Vancouver : University of British Columbia Library
Rights	Attribution-NonCommercial-NoDerivatives 4.0 International
DOI	10.14288/1.0377820
URI	http://hdl.handle.net/2429/69474
Affiliation	Non UBC
Peer Review Status	Unreviewed
Scholarly Level	Researcher
Rights URI	http://creativecommons.org/licenses/by-nc-nd/4.0/
Aggregated Source Repository	DSpace

Open Collections

BIRS Workshop Lecture Videos

The Symmetry Rule for Quantified Boolean Formulas Seidl, Martina

Description

Item Metadata

Item Media

Item Citations and Data

Rights