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 10.1.0 found (12 same-name repos checked); no cached copy. Use another version.
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.
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.
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.
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.
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.
It represent the information of the resolvent, the clauses involved, the renames done, the maximum general unifier (mgu) and the result of the resolvent