@TechReport{Orbe2012,
  author =       "E. Orbe and C. Areces and G. Infante L{\'o}pez",
  institution =  "Facultad De Matem{\'a}tica, Astronom{\'i}a y
                 F{\'i}sica, Universidad Nacional de C{\'o}rdoba",
  title =        "A Note about Modal Symmetries",
  year =         "2012",
  number =       "6/2012",
  series =       "Trabajos de Inform{\'a}tica (Serie A)",
  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.",
}