The module provides the tools for aplying the differents resolution strategies to a set of propositional clauses for verifying its unfeasibility.
It generates the appropriate substitutions for the separation of the clauses
It generates the appropriate substitutions for the separation of the clauses
It searches all the pairs of literals from two clauses that have the same predicate and contrary sign
cfol2AllResolvents. does not have any docs. The module's documentation names it in an @docs line, but the package does not expose it.It represent the graph structure of the tableau
It uses resolution algorithm using shorted clause first heuristic for determining the feasibilibity of a set of clauses. It gives the insatisfactibility and a graph with the resolution path to inconsitence. If clause set is feasible then a graph with only initial nodes is returned.
As first order resolution may not terminate, at most 300 clauses are processed and resolvents of more than 8 literals are discarded: False means that no refutation was found within these bounds.
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.
As first order resolution may not terminate, the search explores at most 100 resolution steps (resolvents of more than 8 literals are discarded): False means that no refutation was found within that bound.
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.
As first order resolution may not terminate, at most 300 clauses are processed and resolvents of more than 8 literals are discarded: False means that no refutation was found within these bounds.
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.
As first order resolution may not terminate, at most 300 clauses are processed and resolvents of more than 8 literals are discarded: False means that no refutation was found within these bounds.
Note: You can render the graph with GraphViz Viewer and resolutionTableauToDOT described at the end.
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.
Express a Resolution Tableau as a string in DOT format that is viewable with a GraphViz Render, with adding custom styles.
It represent the information of the resolvent, the clauses involved, the renames done, the maximum general unifier (mgu) and the result of the resolvent