@TECHREPORT{orbe:note12,
author = {Orbe, E. and Areces, C. and Infante Lopez, G.},
title = {A Note about Modal Symmetries},
institution = {Facultad De Matemática, Astronomía y Física, Universidad Nacional
de Córdoba},
year = {2012},
type = {Trabajos de Informática,},
number = {6/2012,},
abstract = {In this paper we show how permutation of literals can be used to define
symmetries for modal formulas in clausal form. We show that the symmetries
of a modal formula $\varphi$ preserve inference: if $\sigma$ is a
symmetry of $\varphi$ then $\varphi \models \psi$ if and only if
$\varphi \models \sigma(\psi)$. Hence, a modal theorem prover that
has access to the symmetries of the input formula, can use them during
search to cheaply derive symmetric inferences (e.g., as is done during
clause learning in propositional SAT). We also present in a mechanism
to efficiently compute symmetries using graphs automorphisms, and
preliminary empirical results showing that symmetries appear in many
cases in both randomly generated and hand-tailored modal formulas.},
owner = {areces},
series = {A},
timestamp = {2016.10.02}
}