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.

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.

@TECHREPORT{orbe:note12,
author = {Orbe, E. and Areces, C. and Infante Lopez, G.},
title = {A Note about Modal Symmetries},
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