Defines the Resolution Tableau type as a Graph whose node labels are pairs of a bool (indicates if the node is in the original clause set (True) or is a deduction (False)) and the clause considered in the corresponding node; and a edge label is just the literal of source node which is considered in the resolvent.

It gets the resolvent from two clauses by one literal. If it can be performed then it returns the resolvent and the literal considerated in each clause. If the resolvent does not exist it returns Nothing.

cplResolventByPSymb [ ( "p", True ), ( "q", True ) ] [ ( "p", False ), ( "q", True ) ] "p" == Just ( [ ( "q", True ) ], ( "p", True ), ( "p", False ) )


cplResolventByPSymb [ ( "p", True ), ( "q", True ) ] [ ( "p", False ), ( "q", True ) ] "q" == Nothing

It gets all passible resolvents between two clauses. Note that if several resolvents can be performed then all of them are tautologies.

cplAllResolvents [ ( "p", True ), ( "q", True ) ] [ ( "p", False ), ( "q", False ) ]
    == [ ( [ ( "q", False ), ( "q", True ) ], ( "p", True ), ( "p", False ) ), ( [ ( "p", False ), ( "p", True ) ], ( "q", True ), ( "q", False ) ) ]


cplAllResolvents [ ( "p", True ), ( "q", True ) ] [ ( "p", False ), ( "q", True ) ]
    == [ ( [ ( "q", True ) ], ( "p", True ), ( "p", False ) ) ]


cplAllResolvents [ ( "p", True ), ( "q", True ) ] [ ( "q", True ) ] == []

It gets the resolvents between the clauses of a set by the variable given.

csplAllResolventsByPsymb [ [ ( "p", True ), ( "q", True ) ], [ ( "p", False ), ( "q", False ) ], [ ( "p", False ), ( "q", True ) ] ] "p"
    == [ [ ( "q", False ), ( "q", True ) ], [ ( "q", True ) ] ]

It gets all resolvents of each clause of a set with a clause given. It returns a list of a pair with the index of the formula with which the reference clause is resolved and all the resolvents obtained.

csplResolventsByClause [ [ ( "p", True ), ( "q", True ) ], [ ( "p", False ), ( "q", False ) ] ] [ ( "p", False ), ( "q", True ) ]
    == [ ( 0, [ ( [ ( "q", True ) ], ( "p", False ), ( "p", True ) ) ] ), ( 1, [ ( [ ( "p", False ) ], ( "q", True ), ( "q", False ) ) ] ) ]

It gets all possible resolvents each two clauses of the set, and gives it as a clause set ommitting who are the parents and removing duplicated clauses.

csplAllResolvents [ [ ( "p", True ), ( "q", True ) ], [ ( "p", False ), ( "q", False ) ], [ ( "p", False ), ( "q", True ) ] ]
    == [ [ ( "q", False ), ( "q", True ) ], [ ( "p", False ), ( "p", True ) ], [ ( "q", True ) ], [ ( "p", False ) ] ]

It uses saturation resolution algorithm for determining the feasibilibity of a set ot clauses. It gives the insatisfactibility (True:Insat, False:SAT) and the clause set considerated in each step of the algorithm.

cs = [[("p",False),("q",False),("r",True)],[("q",True),("p",True)],[("r",False),("p",True)],[("p",False),("q",True)],[("q",False),("p",True)],[("p",False),("r",False)]]


csplSaturationResolution  cs
    == (True,[[[("p",False),("q",False),("r",True)],[("q",True),("p",True)],[("r",False),("p",True)],[("p",False),("q",True)],[("q",False),("p",True)],[("p",False),("r",False)],[("q",False),("q",True),("r",True)],[("p",False),("p",True),("r",True)],[("q",False),("r",False),("r",True)],[("p",False),("p",True),("q",False)],[("p",False),("r",True)],[("q",True)],...

It uses regular resolution algorithm for determining the feasibilibity of a set ot clauses. It gives the insatisfactibility (True:Insat, False:SAT) and the clause set considerated in each step of the algorithm.

csplRegularResolution [ "p", "q", "r" ] cs
    == ( True, [ [ [ ( "p", False ), ( "q", False ), ( "r", True ) ], [ ( "q", True ), ( "p", True ) ], [ ( "r", False ), ( "p", True ) ], [ ( "p", False ), ( "q", True ) ], [ ( "q", False ), ( "p", True ) ], [ ( "p", False ), ( "r", False ) ] ], [ [ ( "q", False ), ( "q", True ), ( "r", True ) ], [ ( "q", False ), ( "r", False ), ( "r", True ) ], [ ( "q", True ) ], [ ( "q", True ), ( "r", False ) ], [ ( "q", False ), ( "r", True ) ], [ ( "q", False ), ( "q", True ) ], [ ( "r", False ) ], [ ( "q", False ), ( "r", False ) ] ], [ [ ( "r", False ) ], [ ( "r", False ), ( "r", True ) ], [ ( "r", True ) ], [ ( "r", False ) ] ], [ [] ] ] )

It uses resolution algorithm using shortes clause first heuristic for determining the feasibilibity of a set of clauses. It gives the insatisfactibility (True:Insat, False:SAT) and a graph with the resolution path to inconsitence. If clause set is feasible then a graph with only initial nodes is returned.

res_SCFResolution = csplSCFResolution cs
Tuple.first res_SCFResolution == True
res_SCFResolution |> Tuple.second |> resolutionTableauToDOT
    == "digraph G {\n  rankdir=TB\n  graph []\n  node [shape=box, color=black]\n  edge [dir=none, color=blue, fontcolor=blue]\n\n  1 -> 6 [label=\"q\"]\n  2 -> 8 [label=\"p\"]\n  3 -> 10 [label=\"q\"]\n  5 -> 6 [label=\"¬ q\"]\n  6 -> 11 [label=\"p\"]\n  7 -> 8 [label=\"¬ p\"]\n  8 -> 12 [label=\"¬ r\"]\n  9 -> 10 [label=\"¬ q\"]\n  10 -> 11 [label=\"¬ p\"]\n  11 -> 12 [label=\"r\"]\n\n  1 [label=\"{p,q}\"]\n  2 [label=\"{p,¬ r}\"]\n  3 [label=\"{¬ p,q}\"]\n  5 [label=\"{p,¬ q}\"]\n  6 [label=\"{p}\"]\n  7 [label=\"{¬ p,¬ r}\"]\n  8 [label=\"{¬ r}\"]\n  9 [label=\"{¬ p,¬ q,r}\"]\n  10 [label=\"{¬ p,r}\"]\n  11 [label=\"{r}\"]\n  12 [label=\"□\"]\n\n  {rank=same; 1;2;3;5;7;9;}\n}"

Note: You can render the graph with GraphViz Viewer and resolutionTableauToDOt as we show in the example above.

It uses linear resolution algorithm using shortest clause first heuristic for determining the feasibilibity of a set of clauses. It gives the insatisfactibility (True:Insat, False:SAT) and a graph with the resolution path to inconsitence. If clause set is feasible then a graph with only initial nodes is returned.

res_SCFLinearResolution = csplSCFLinearResolution cs
Tuple.first res_SCFLinearResolution == True
res_SCFLinearResolution |> Tuple.second |> resolutionTableauToDOT
    == "digraph G {\n  rankdir=TB\n  graph []\n  node [shape=box, color=black]\n  edge [dir=none, color=blue, fontcolor=blue]\n\n  1 -> 8 [label=\"p\"]\n  3 -> 8 [label=\"¬ p\"]\n  4 -> 9 [label=\"¬ q\"]\n  5 -> 10 [label=\"¬ p\"]\n  6 -> 11 [label=\"r\"]\n  8 -> 9 [label=\"q\"]\n  8 -> 12 [label=\"q\"]\n  9 -> 10 [label=\"p\"]\n  9 -> 13 [label=\"p\"]\n  10 -> 11 [label=\"¬ r\"]\n  11 -> 12 [label=\"¬ q\"]\n  12 -> 13 [label=\"¬ p\"]\n\n  1 [label=\"{p,q}\"]\n  3 [label=\"{¬ p,q}\"]\n  4 [label=\"{p,¬ q}\"]\n  5 [label=\"{¬ p,¬ r}\"]\n  6 [label=\"{¬ p,¬ q,r}\"]\n  8 [label=\"{q}\"]\n  9 [label=\"{p}\"]\n  10 [label=\"{¬ r}\"]\n  11 [label=\"{¬ p,¬ q}\"]\n  12 [label=\"{¬ p}\"]\n  13 [label=\"□\"]\n  14 [label=\"{p,¬ r}\"]\n\n  {rank=same; 1;3;4;5;6;14;}\n}"

Note: You can render the graph with GraphViz Viewer and resolutionTableauToDOT described at the end.

It uses positive resolution algorithm using shortest clause first heuristic for determining the feasibilibity of a set of clauses. It gives the insatisfactibility (True:Insat, False:SAT) and a graph with the resolution path to inconsitence. If clause set is feasible then a graph with only initial nodes is returned.

res_SCFPositiveResolution = csplSCFPositiveResolution cs
Tuple.first res_SCFPositiveResolution == True
res_SCFPositiveResolution |> Tuple.second |> resolutionTableauToDOT
    == "digraph G {\n  rankdir=TB\n  graph []\n  node [shape=box, color=black]\n  edge [dir=none, color=blue, fontcolor=blue]\n\n  1 -> 8 [label=\"p\"]\n  1 -> 9 [label=\"q\"]\n  3 -> 8 [label=\"¬ p\"]\n  4 -> 9 [label=\"¬ q\"]\n  5 -> 14 [label=\"¬ p\"]\n  6 -> 12 [label=\"¬ q\"]\n  8 -> 12 [label=\"q\"]\n  9 -> 14 [label=\"p\"]\n  9 -> 15 [label=\"p\"]\n  12 -> 15 [label=\"¬ p\"]\n  14 -> 17 [label=\"¬ r\"]\n  15 -> 17 [label=\"r\"]\n\n  1 [label=\"{p,q}\"]\n  3 [label=\"{¬ p,q}\"]\n  4 [label=\"{p,¬ q}\"]\n  5 [label=\"{¬ p,¬ r}\"]\n  6 [label=\"{¬ p,¬ q,r}\"]\n  8 [label=\"{q}\"]\n  9 [label=\"{p}\"]\n  12 [label=\"{¬ p,r}\"]\n  14 [label=\"{¬ r}\"]\n  15 [label=\"{r}\"]\n  17 [label=\"□\"]\n  18 [label=\"{p,¬ r}\"]\n\n  {rank=same; 1;3;4;5;6;18;}\n}"

Note: You can render the graph with GraphViz Viewer and resolutionTableauToDOT described at the end.

It uses negative resolution algorithm using shortest clause first heuristic for determining the feasibilibity of a set of clauses. It gives the insatisfactibility (True:Insat, False:SAT) and a graph with the resolution path to inconsitence. If clause set is feasible then a graph with only initial nodes is returned.

res_SCFNegativeResolution = csplSCFNegativeResolution cs
Tuple.first res_SCFNegativeResolution == True
res_SCFNegativeResolution |> Tuple.second |> resolutionTableauToDOT
    == "digraph G {\n  rankdir=TB\n  graph []\n  node [shape=box, color=black]\n  edge [dir=none, color=blue, fontcolor=blue]\n\n  1 -> 16 [label=\"p\"]\n  2 -> 10 [label=\"p\"]\n  3 -> 14 [label=\"q\"]\n  4 -> 17 [label=\"p\"]\n  5 -> 10 [label=\"¬ p\"]\n  6 -> 12 [label=\"r\"]\n  10 -> 12 [label=\"¬ r\"]\n  12 -> 14 [label=\"¬ q\"]\n  14 -> 16 [label=\"¬ p\"]\n  14 -> 17 [label=\"¬ p\"]\n  16 -> 19 [label=\"q\"]\n  17 -> 19 [label=\"¬ q\"]\n\n  1 [label=\"{p,q}\"]\n  2 [label=\"{p,¬ r}\"]\n  3 [label=\"{¬ p,q}\"]\n  4 [label=\"{p,¬ q}\"]\n  5 [label=\"{¬ p,¬ r}\"]\n  6 [label=\"{¬ p,¬ q,r}\"]\n  10 [label=\"{¬ r}\"]\n  12 [label=\"{¬ p,¬ q}\"]\n  14 [label=\"{¬ p}\"]\n  16 [label=\"{q}\"]\n  17 [label=\"{¬ q}\"]\n  19 [label=\"□\"]\n\n  {rank=same; 1;2;3;4;5;6;}\n}"

Note: You can render the graph with GraphViz Viewer and resolutionTableauToDOT described at the end.

It uses unitary resolution algorithm using shortest clause first heuristic for determining the feasibilibity of a set of clauses. It gives the insatisfactibility (True:Insat, False:SAT) and a graph with the resolution path to inconsitence. If clause set is feasible then a graph with only initial nodes is returned.

res_SCFUnitaryResolution = csplSCFUnitaryResolution cs
Tuple.first res_SCFUnitaryResolution == False
res_SCFUnitaryResolution |> Tuple.second |> resolutionTableauToDOT
    == "digraph G {\n  rankdir=TB\n  graph []\n  node [shape=box, color=black]\n  edge [dir=none, color=blue, fontcolor=blue]\n\n\n\n  1 [label=\"{¬ p,¬ q,r}\"]\n  2 [label=\"{p,q}\"]\n  3 [label=\"{p,¬ r}\"]\n  4 [label=\"{¬ p,q}\"]\n  5 [label=\"{p,¬ q}\"]\n  6 [label=\"{¬ p,¬ r}\"]\n\n  {rank=same; 1;2;3;4;5;6;}\n}"

Note: You can render the graph with GraphViz Viewer and resolutionTableauToDOT described at the end.

It uses resolution by entries algorithm using shortest clause first heuristic for determining the feasibilibity of a set of clauses. It gives the insatisfactibility (True:Insat, False:SAT) and a graph with the resolution path to inconsitence. If clause set is feasible then a graph with only initial nodes is returned.

res_SCFByEntriesResolution = csplSCFByEntriesResolution cs
Tuple.first res_SCFByEntriesResolution == False
res_SCFByEntriesResolution |> Tuple.second |> resolutionTableauToDOT
    == "digraph G {\n  rankdir=TB\n  graph []\n  node [shape=box, color=black]\n  edge [dir=none, color=blue, fontcolor=blue]\n\n\n\n  1 [label=\"{¬ p,¬ q,r}\"]\n  2 [label=\"{p,q}\"]\n  3 [label=\"{p,¬ r}\"]\n  4 [label=\"{¬ p,q}\"]\n  5 [label=\"{p,¬ q}\"]\n  6 [label=\"{¬ p,¬ r}\"]\n\n  {rank=same; 1;2;3;4;5;6;}\n}"

Note: You can render the graph with GraphViz Viewer and resolutionTableauToDOT described at the end.

It gives a string representation in Latex notation for a list of clauseSets. It must be displayed in a math environment

It gives a string representation for a list of clauseSets

Express a Resolution Tableau as a string.

Express a Resolution 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.