A Note about Modal Symmetries

E. Orbe, C. Areces, and G. Infante López. A Note about Modal Symmetries. Technical Report 6/2012, Facultad De Matemática, Astronom\'ia y F\'isica, Universidad Nacional de Córdoba, 2012.

Download

[pdf] 

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.

BibTeX

@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.",
}