1. Atom: The Atom is the datatype used to describe Atomic Sentences or propositions. These are basically represented as a string. 2. Literal: Literals correspond to either atoms or negations of atoms. In this implementation each literal is represented as a pair consisting of a boolean value, indicating the polarity of the Atom, and the actual Atom. Thus, the literal ‘P’ is represented as (True,"P") whereas its negation ‘-P’ as (False,"P"). 2 3. Clause: A Clause is a disjunction of literals, for example PvQvRv-S. In this implementation this is represented as a list of Literals. So the last clause would be [(True,"P"), (True,"Q"), (True,"R"),(False,"S")]. 4. Formula: A Formula is a conjunction of clauses, for example (P vQ)^(RvP v-Q)^(-P v-R). This is the CNF form of a propositional formula. In this implementation this is represented as a list of Clauses, so it is a list of lists of Literals. Our above example formula would be [[(True,"P"), (True,"Q")], [(True,"R"), (True,"P"), (False,"Q")], [(False, "P"), (False,"P")]]. 5. Model: A (partial) Model is a (partial) assignment of truth values to the Atoms in a Formula. In this implementation this is a list of (Atom, Bool) pairs, ie. the Atoms with their assignments. So in the above example of type Formula if we assigned true to P and false to Q then our model would be [("P", True),("Q", False)] -- View this message in context: http://haskell.1045720.n5.nabble.com/Update2-tp3392490p3392589.html Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com.