Equisatisfiability is generally used in the context of translating formulae, so that one can define a translation to be correct if the original and resulting formulae are equisatisfiable. Examples of translations involving this concept are Skolemization and some translations into Conjunctive normal form. The Davis-Putnam algorithm removes, at each step, a variable from a formula, generating a formula that is equisatisfiable with the original one.
Examples
A translation from propositional logic into propositional logic in which every binary disjunction is replaced by , where is a new variable (one for each replaced disjunction) is a transformation in which satisfiability is preserved: the original and resulting formulae are equisatisfiable. Note that these two formulae are not equivalent: the first formula has the model in which is true while and are false, and this is not a model of the second formula, in which has to be true in this case.
This article is licensed under the GNU Free Documentation License.
Last updated on Friday February 22, 2008 at 08:40:04 PST (GMT -0800)
View this article at Wikipedia.org - Edit this article at Wikipedia.org - Donate to the Wikimedia Foundation
Copyright © 2008, Dictionary.com, LLC. All rights reserved.