Result: Local symmetries in propositional logic

Title:
Local symmetries in propositional logic
Authors:
ARAI, N. H, URQUHART, A
Source:
TABLEAUX 2000 : automated reasoning with analytic tableaux and related methods (St Andrews, 3-7 July 2000)Lecture notes in computer science. :40-51
Publisher Information:
Berlin: Springer, 2000.
Publication Year:
2000
Physical Description:
print, 16 ref
Original Material:
INIST-CNRS
Subject Terms:
Computer science, Informatique, Sciences exactes et technologie, Exact sciences and technology, Sciences appliquees, Applied sciences, Informatique; automatique theorique; systemes, Computer science; control theory; systems, Intelligence artificielle, Artificial intelligence, Divers, Miscellaneous, Complexité programme, Program complexity, Complejidad programa, Logique propositionnelle, Propositional logic, Lógica proposicional, Programmation logique, Logical programming, Programación lógica, Programmation mathématique, Mathematical programming, Programación matemática, Règle inférence, Inference rule, Regla inferencia
Document Type:
Conference Conference Paper
File Description:
text
Language:
English
Author Affiliations:
Department of Computer Science, Faculty of Information Sciences, Hiroshima City University, 3-4-1 Ozuka-higashi, Asaminami-ku, Hiroshima 731-31, Japan
Departments of Philosophy and Computer Science, University of Toronto, Toronto, Ontario M5S 1A1, Canada
ISSN:
0302-9743
Access URL:
http://pascal-francis.inist.fr/vibad/index.php?action=search&terms=1379938
Rights:
Copyright 2000 INIST-CNRS
CC BY 4.0
Sauf mention contraire ci-dessus, le contenu de cette notice bibliographique peut être utilisé dans le cadre d’une licence CC BY 4.0 Inist-CNRS / Unless otherwise stated above, the content of this bibliographic record may be used under a CC BY 4.0 licence by Inist-CNRS / A menos que se haya señalado antes, el contenido de este registro bibliográfico puede ser utilizado al amparo de una licencia CC BY 4.0 Inist-CNRS
Notes:
Computer science; theoretical automation; systems
Accession Number:
edscal.1379938
Database:
PASCAL Archive

Further Information

The symmetry rule in propositional logic allows the exploitation of symmetries present in a problem. In the context of resolution, the rule enables the shortening of refutations by using symmetries present in an initial set of clauses. These symmetries can be local or global. The present paper proves that the local symmetry rule is strictly more powerful than the global symmetry rule. It also exhibits sets of clauses that show exponential lower bounds for the local symmetry rule, where the symmetry group consists of all variable permutations. These examples remain exponentially hard even when the symmetry group is enlarged to include complementation. Examples are exhibited in which resolution with the global symmetry rule has an exponential speed-up with respect to the cutting plane refutation system.