GUI for Resolution Problem Solving
Windows and Mac executables can be downloaded from the Release section (v1.0.0).
Run resolute.exe
Note: If the executable doesn't run correctly, run python resolute.py in command prompt
Using Python 3, run python resolute.py in the terminal.
Download the Mac app and run
Note: If this doesn't work, run python resolute.py in the terminal (must be Python 3)
Use the "Add Sentence" button to add the required number of sentences, and "Remove Sentence" to remove a sentence.
Enter the sentences. The following symbols can be used:
v - disjunction (logical or)
^ - conjunction (logical and)
-> - conditional (implies)
<-> - biconditional (if and only if)
~ - negation
Make sure to enter the negation of the conclusion in the "Therefore" sentence (at the bottom, with the therefore symbol).
When finished entering the sentences, press the Solve button, and your resolution graph will appear.
The File menu has Save and Open options, where the current file can be saved as a .reso file and reopened.
Example:
