A Note about Modal Symmetries

Orbe, E., Areces, C., and Infante Lopez, G.. A Note about Modal Symmetries. Technical Report 6/2012,, Facultad De Matemática, Astronomía y Física, 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: (download)

@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}
}

Generated by bib2html.pl (written by Patrick Riley) on Sun Oct 02, 2016 17:05:49