Merge branch 'main' of https://github.com/Claydough6/gui_resolution i…

…nto main

README.md

@@ -1,2 +1,46 @@
 # gui_resolution
 Standalone logical resolution application for Computability and Logic RPI course final project.
+
+Authors: Clay Bell and Kevin Khaghani
+
+## How to Use:
+Note: this is found in help.txt as well. It is displayed when the help menu is clicked in the app.
+
+How to use the application:
+
+1. Add premises to the list with the 'Add Premise' button.
+  -  you can add as many premises as you want
+  -  you can only have one conclusion 
+
+2. Delete premises by clicking on the premise then clicking the 'Delete Premise' button.
+
+3. Edit the premises or conclusion by double clicking on the statement you want to edit.
+  -  type in the new statement
+  -  hit 'Enter' to save your input
+  -  hit 'Escape' to stop editing without saving
+
+4. To add clauses to the resolution screen, shift-click on an empty space to create a new statement box. 
+  -  edit the text to add a clause
+
+5. To delete a clause, select it and hit the 'delete' key.
+  -  you cannot undo this as of now, so be careful
+
+6. Clauses can be selected to modify their properties. To select a clause, click on the clause (or space around it). 
+  -  it will raise up to indicate it has been selected
+  -  click the clause again or anywhere else to deselect it
+
+7. To move a clause, click the side of the clause and drag it around the screen.
+
+8. To derive a clause from another, select the derived clause. Then select the clauses it comes from.
+  -  arrows will be drawn to show the relationship.
+  -  click again to undo a derivation relationship
+
+9. To derive a top level clause from a premise statement, select a clause then click a premise to select it.
+  -  this only works for clauses that aren't linked to others
+  -  click the premise again to unlink it 
+  -  click a different premise to change which is linked
+
+10. To check derivations, click the 'Verify Resolution' button.
+  -  this will check each premise, the conclusion, and the resolution steps
+  -  any errors will be displayed in the error window
+  -  if the derivation is successful the labels will change to 'valid!'