Reference no: EM132979924
The logic of equality. Is it possible to assign values to the variables a, b, c, and d, so that the formula (a=b)∧(b=c)∧(c=d)∧¬(a=d) is true? How about the formula (a=c) ⇔ (¬(a=b)∨¬(b=c))? These are examples of satisfiability questions in the system of equality logic. A formula in equality logic includes a collection of variables, such as a, b, c, and d. These variables are related to one another by equalities, such as (a=b). Equalities are assembled into formulas using connectives, like the ones we are familiar with from propositional and predicate logic: ∧, ∨, ¬, ⇒, ⇔, and ⊕. An equality logic formula is satisfiable if there is some assignment of values to its variables that makes the formula evaluate to true, under the usual semantics of equality and the logical connectives.
Task overview. In this challenge, you will complete an implementation of a satisfiability decision procedure for equality logic formulas. The decision procedure will work as follows:
1. You will devise a way of modelling an equality logic formula as an equisatisfiable propositional logic formula, using the strategy below.
2. You will implement this modelling strategy as a Haskell function that translates equality logic formulas into propositional logic formulas, supported by some scaffolding code we provide. We break this step down into four implementation tasks, described below.
3. We provide a satisfiability algorithm for propositional logic, which will decide whether your propositional formula (and thus also the original equality logic formula) is satisfiable or not.
The strategy. The key to satisfying an equality logic formula in is knowing which variables to assign to the same values. If we know whether or not each pair of variables shares a value, we have all we need to evaluate the formula. If this information were to be encoded in propositional logic, what propositions might we use? To encode an equality logic formula in propositional logic is to use these propositions to capture the logical structure of the original formula, along with the special properties of the equality relation, in a single propositional formula. The four tasks below will guide you to capturing this strucure.
Task A. Using your propositional variables, implement a Haskell function to encode the logical constraints implied by an equality logic formula's connectives as a formula in propositional logic.
Task B. Equality is a reflexive relation: A variable always equals itself, so a formula like (a=a) is always true in equality logic. Using your propositional variables, implement a Haskell function to encode the constraints implied by this property as a formula in propositional logic.
Task C. Equality is also a symmetric relation: Equality can't be true in one ‘direction' and not the other. (a=b) and (b=a) are equivalent in equality logic. Using your propositional variables, implement a Haskell function to encode the constraints implied by this property as a formula in propositional logic. Hint: Depending on your propositional variables, this may be a short formula.
Task D. Finally, equality is a transitive relation: Equalities chain together. If we know (a=b) and (b=c), then we must have (a=c) too, even if this is not specified directly in an equality logic formula. Using your propositional variables, implement a Haskell function to encode the constraints implied by this property as a formula in propositional logic. Hint: For each individual group of three variables, consider all of the ways in which the transitive property could affect the formula.