Unavailable. Nobody can download this version any more, with elm or with the Lamdera compiler: github.com/vicramgon/logicus is gone (deleted or private); Software Heritage not asked yet (this run's --swh-calls were used up); no fork with tag 1.0.0 found (12 same-name repos checked); no cached copy. Use another version.
The module provides the tools for applying the DPLL algorithm to solve the fesibility of a set of propositional clauses and calculates its models if they exist.
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 cs2Gets 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}"
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.