The symmetry rule in propositional logic
type: Item
instance of: scholarly article
title: The symmetry rule in propositional logic
zbMATH Open document ID: 0938.03023
DOI: 10.1016/S0166-218X(99)00039-6
author: Alasdair Urquhart
published in: Discrete Applied Mathematics
publication date: 2000-02-14T00:00:00Z
review text: The addition of the symmetry rule to the resolution proof system sometimes allows considerable shortening in the length of refutations. An exponential lower bound on the size of resolution refutations using two forms of a global symmetry rule is shown. The paper also discusses the relationship of symmetry rules to the extension rule that allows the use of abbreviative definitions in proofs. Also, symmetry of random clause sets is considered.
Mathematics Subject Classification ID: 03B35
Mathematics Subject Classification ID: 03B05
Mathematics Subject Classification ID: 03F20
Mathematics Subject Classification ID: 68T15
zbMATH DE Number: 1389870
zbMATH Keywords: symmetry rule
zbMATH Keywords: exponential lower bound on the size of resolution refutations
zbMATH Keywords: extension rule
zbMATH Keywords: random clause
MaRDI profile type: Publication
cites work: Resolution proofs of generalized pigeonhole principles
cites work: The tail of the hypergeometric distribution
cites work: Many hard examples for resolution
cites work: The relative efficiency of propositional proof systems
cites work: Explicit constructions of linear-sized superconcentrators
cites work: On the complexity of regular resolution and the Davis-Putnam procedure
cites work: The intractability of resolution
cites work: Q5593643
cites work: Propositional proof systems, the consistency of first order theories and the complexity of computations
cites work: Short proofs for tricky formulas
cites work: Hard examples for resolution
cites work: The Complexity of Propositional Proofs
cites work: Graphs on unlabelled nodes with a given number of edges
Wikidata QID: Q126297728
description: scientific article; zbMATH DE number 1389870