<table cellspacing="0" cellpadding="0" border="0" ><tr><td valign="top" style="font: inherit;"><br><blockquote style="border-left: 2px solid rgb(16, 16, 255); margin-left: 5px; padding-left: 5px;"><br><div id="yiv1077113142"><table border="0" cellpadding="0" cellspacing="0"><tbody><tr><td style="font: inherit;" valign="top"><blockquote style="border-left: 2px solid rgb(16, 16, 255); margin-left: 5px; padding-left: 5px;"><div id="yiv1077113142"><table border="0" cellpadding="0" cellspacing="0"><tbody><tr><td style="font: inherit;" valign="top">I need help with two functions....first this is the curent code :<a rel="nofollow" target="_blank" href="http://pastebin.com/UPATJ0r"><span class="yiv1077113142yshortcuts" id="yiv1077113142lw_1296754525_0">http://pastebin.com/UPATJ0r</span></a><br>->Function 1)<span class="yiv1077113142pln">removeTautologies </span><span class="yiv1077113142pun">::</span><span class="yiv1077113142pln"> Formula</span><span
class="yiv1077113142pun">-></span>Formula <br>If in a clause, a literal and its negation are found, it means that the clause will be true, regardless of the value
finally assigned to that propositional variable. Consider the following example:
(A v B v -A) ^ (B v C v A)
The first clause contains the literals A and -A. This means that the clause will always be true, in which case
it can be simplify the whole set to simply (B v C v A) .<br>I was tinking of using something like<br> <span class="yiv1077113142pln">removeTautologies (f:fs)=filter rTf:</span><span class="yiv1077113142pln">removeTautologies fs<br>
where rT-is supposed to take the firs Literal from the clasue and
search for a similar one,if one si found we compare the values if not
the we go to the second literal.<br></span>->Function 2)<code><span class="yiv1077113142pln">pureLiteralDeletion </span><span class="yiv1077113142pun">::</span><span class="yiv1077113142pln"> Formula</span><span class="yiv1077113142pun">-></span><span class="yiv1077113142pln">Formula<br>This is a little bit complicate but from What I get this</span></code> function is suppose to implement a simplification step that assumes
as true any atom in a formula that appears exclusively in a positive or
negative form (not both). Consider the formula:
(P v Q v R) ^ (P v Q v -R) ^ (-Q v R)
Note that in this formula P is present but -P is not. Using Pure Literal
Deletion it can be assumed that the value of P will be True thus
simplifying the formula to (-Q v R). If the literal were false then the
literal would simply be deleted from the clauses it appears in. In that
case any satisfying model for the resulting formula would also be a
satisfying model for the formula when we assume that the literal is true.</td></tr></tbody></table><br>
</div></blockquote></td></tr></tbody></table><br>
</div></blockquote></td></tr></table><br>