Defines the DPLL Tableau type as a Graph whose node labels are pairs of an integer (0: internal node, 1: open leaf, -1: closed leaf) and the set of PL clauses considered in the corresponding node; and a edge label is just the literal which is propagated.

It computes DPLL algorithm given the result and the process as a DPLL Tableau

cs1 =
    [ [ Neg (Atom "r"), Atom "p", Atom "q" ], [ Neg (Atom "p"), Atom "r" ], [ Neg (Atom "q"), Atom "r" ], [ Neg (Atom "s"), Atom "p" ], [ Atom "s", Atom "r", Atom "t" ], [ Neg (Atom "p") ], [ Neg (Atom "q") ], [ Neg (Atom "t") ] ]


t1 =
    dpll cs1


cs2 =
    [ [ Neg (Atom "r"), Atom "p", Atom "q" ], [ Neg (Atom "p"), Atom "r" ], [ Neg (Atom "q"), Atom "r" ], [ Neg (Atom "s"), Atom "p" ], [ Atom "s", Atom "r", Atom "t" ], [ Neg (Atom "p") ] ]


t2 =
    dpll cs2

Gets the Tableau DPLL models. It requires a set of reference symbols that are added to those present in the tableau since in the transformation to clauses some symbols may have disappeared.

dpllTableauModels [] t1 == []


dpllTableauModels [] t2 == [ [ "q", "r" ], [ "q", "r", "t" ], [ "t" ] ]

Express a DPLL Tableau as a string.

dpllTableauToString t1 == "Graph [Node 0 ({¬ r, p, q}, {¬ s, p}, {s, r, t}, {¬ p}, {¬ q}, {¬ t}), Node 1 ({¬ r, q}, {¬ s}, {s, r, t}, {¬ q}, {¬ t}), Node 2 ({¬ r, q}, {r, t}, {¬ q}, {¬ t}), Node 3 ({¬ r}, {r, t}, {¬ t}), Node 4 ({t}, {¬ t}), Node 5 (□)] [Edge 4->5 (t), Edge 3->4 (¬ r), Edge 2->3 (¬ q), Edge 1->2 (¬ s), Edge 0->1 (¬ p)]"


dpllTableauToString t2 == "Graph [Node 0 ({¬ r, p, q}, {¬ q, r}, {¬ s, p}, {s, r, t}, {¬ p}), Node 1 ({¬ r, q}, {¬ q, r}, {¬ s}, {s, r, t}), Node 2 ({¬ r, q}, {¬ q, r}, {r, t}), Node 3 ({q}), Node 4 (◯), Node 5 ({¬ q}, {t}), Node 6 ({t}), Node 7 (◯)] [Edge 6->7 (t), Edge 5->6 (¬ q), Edge 3->4 (q), Edge 2->5 (¬ r), Edge 2->3 (r), Edge 1->2 (¬ s), Edge 0->1 (¬ p)]"

Express a DPLL Tableau as a string in DOT format that is viewable with a GraphViz Render.

Note: If you are using elm repl, before introducing the code you must replace \n by \n and \" by " in a simple text editor.

dpllTableauToDOT t1 == "digraph G {\n  rankdir=TB\n  graph []\n  node [shape=box, color=black]\n  edge [dir=none, color=blue, fontcolor=blue]\n\n  0 -> 1 [label=\"¬ p\"]\n  1 -> 2 [label=\"¬ s\"]\n  2 -> 3 [label=\"¬ q\"]\n  3 -> 4 [label=\"¬ r\"]\n  4 -> 5 [label=\"t\"]\n\n  0 [label=\"{¬ r, p, q}, {¬ s, p}, {s, r, t}, {¬ p}, {¬ q}, {¬ t}\"]\n  1 [label=\"{¬ r, q}, {¬ s}, {s, r, t}, {¬ q}, {¬ t}\"]\n  2 [label=\"{¬ r, q}, {r, t}, {¬ q}, {¬ t}\"]\n  3 [label=\"{¬ r}, {r, t}, {¬ t}\"]\n  4 [label=\"{t}, {¬ t}\"]\n  5 [label=\"□\"]\n}"


dpllTableauToDOT t2 = "digraph G {\n  rankdir=TB\n  graph []\n  node [shape=box, color=black]\n  edge [dir=none, color=blue, fontcolor=blue]\n\n  0 -> 1 [label=\"¬ p\"]\n  1 -> 2 [label=\"¬ s\"]\n  2 -> 3 [label=\"r\"]\n  2 -> 5 [label=\"¬ r\"]\n  3 -> 4 [label=\"q\"]\n  5 -> 6 [label=\"¬ q\"]\n  6 -> 7 [label=\"t\"]\n\n  0 [label=\"{¬ r, p, q}, {¬ q, r}, {¬ s, p}, {s, r, t}, {¬ p}\"]\n  1 [label=\"{¬ r, q}, {¬ q, r}, {¬ s}, {s, r, t}\"]\n  2 [label=\"{¬ r, q}, {¬ q, r}, {r, t}\"]\n  3 [label=\"{q}\"]\n  4 [label=\"◯\"]\n  5 [label=\"{¬ q}, {t}\"]\n  6 [label=\"{t}\"]\n  7 [label=\"◯\"]\n}"