PatrickM patrickm7860 at yahoo.co.uk
Sat Feb 19 20:57:59 CET 2011

```   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