2019 Submission

2016/README.md

@@ -0,0 +1,20 @@
+# Handy Logic Doodahs-Truth Trees
+## Authors
+2016:
+Matt Peveler
+
+## About
+This is a flask app (with a python module backing it) that can be used to solve generate a truth tree for any given number of formulas and one goal. This is part of the handy logic doodahs series of Automated Theorem Provers.
+
+![Flask App](https://raw.githubusercontent.com/MasterOdin/TruthTrees/master/static/screenshot.png)
+
+It uses a functional format for inputting logical formulas. This is the base identity for inputs:
+```
+A
+not(A)
+and(A, B)
+or(A, B)
+if(A, B)
+iff(A, B)
+```
+where `A` and `B` can either be atomic statements or a functional operator. All operators are either unary (not) or binary (and, or, if, iff) and there is no support for a generalized notation. This means that ```and(A, B, C)``` will thrown an error.

2019/LICENSE.md

@@ -0,0 +1,21 @@
+The MIT License (MIT)
+
+Copyright (c) 2016 Matthew Peveler
+
+Permission is hereby granted, free of charge, to any person obtaining a copy
+of this software and associated documentation files (the "Software"), to deal
+in the Software without restriction, including without limitation the rights
+to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all
+copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
+SOFTWARE.

2019/README.md

@@ -0,0 +1,30 @@
+# Handy Logic Doodahs-Truth Trees Manual Creation
+## Authors
+2016:
+Matt Peveler
+
+2019:
+Ji hann Hong
+Terry Nguyen
+
+## About
+This is a flask app (with a python module backing it) that can be used to manually create a truth tree. 
+
+This project is built off of Matt Peveler's Handy Logic Doodas-Truth Trees program.
+https://github.com/Bram-Hub/HLD-TT
+
+GitLab repository.
+https://gitlab.com/GHanSolo42/truth_tree
+
+![Flask App](https://raw.githubusercontent.com/MasterOdin/TruthTrees/master/static/screenshot.png)
+
+It uses a functional format for inputting logical formulas. This is the base identity for inputs:
+```
+A
+not(A)
+and(A, B)
+or(A, B)
+if(A, B)
+iff(A, B)
+```
+where `A` and `B` can either be atomic statements or a functional operator. All operators are either unary (not) or binary (and, or, if, iff) and there is no support for a generalized notation. This means that ```and(A, B, C)``` will thrown an error.

2019/cli_manual_entry

@@ -0,0 +1,49 @@
+$ Welcome to the truth tree project
+
+tree/ $ make_root
+Creating Root
+type \stop to stop adding statements
+
+tree/ $ Statement 1 -> A
+tree/ $ Statement 2 -> iff(A, B)
+tree/ $ Statement 3 -> \stop
+Done. Going to root
+tree/root/ $ \print
+(representation of tree)
+tree/root/ $ cd ../
+tree/ $ cd root
+tree/root/ $ 
+tree/root/ $ \branch
+Creating branch based on what?
+
+1: A
+2: iff(A, B)
+
+tree/root/ $ Branching on -> 2
+Creating branches 2.1 and 2.2
+tree/root/2.1/ $ cd ../
+tree/root/ $ cd 2.2
+tree/root/2.2/ $ make_statements
+Adding statements
+type \stop to stop adding statements
+tree/root/2.2/ $ -> A
+tree/root/2.2/ $ -> B
+tree/root/2.2/ $ -> \stop
+tree/root/2.2/ $ \open
+tree/root/2.2/ marked as open
+tree/root/2.2/ (open) $ cd ../
+tree/root/ $ cd 2.1/
+tree/root/2.1/ $ make_statements
+Adding statements
+type \stop to stop adding statements
+tree/root/2.1/ $ -> ~A
+tree/root/2.1/ $ -> ~B
+tree/root/2.1/ $ -> \stop
+tree/root/2.1/ $ \close
+tree/root/2.1/ marked as open
+tree/root/2.1/ (closed) $ verify
+Success!
+
+
+
+

2019/developmentSpring2019.md

@@ -0,0 +1,37 @@
+# Goal
+The goal of the project is to create a replacement or alternative to the
+java TruthTree generator on BramHub.
+
+# Development
+Currently, the program allows for basic commands for making the truth tree.
+Compared to the java program, users can checkmark off formulas after it has been successfully decompose.  
+
+For this semester, the front end and back end was develop using Matt Peveler work as a base. The tree class was altered to allow for manual editing and verification for marking parents and checkmarking was added. The front end uses flask to give a view of the tree.
+
+## Currently Known Bugs
+* Mark_close is not edit safe
+    * If a user closes a node based on two formula, and then delete one of the
+    formula, the node would still be marked as closed.
+* Mark_open is not edit safe
+    * If a user were to verify a branch is open, then delete or add a formula
+    which violate the branch being open, the branch would remain open.
+* Form Resubmission is still allowed
+
+# Possible Future Improvements
+* Use a better formula parser
+    * forsetti isn't the most reliable
+* Print out the parent formula id after marking parent in Flask App
+    * A Quality of Life change to allow users to know which formula has which parents
+* More commands
+    * Add commands such as edit and export
+* Export and Import  Tree
+    * In theory, the history in the TreeShell class can be exported text file
+    * Then this text file can be used to recreate the tree
+* Create an adapter that takes in formula input and change it into something forsetti can parse
+    * Allow user to type (a & b) instead of and(a,b)
+* Refactor to eliminate duplicates due to color classes, styles
+* Re-integrate auto-solve truth tree from original fork
+* Center the Tree in CSS
+* Bi-conditionals should be tested more
+
+

2019/how to use.md

@@ -0,0 +1,100 @@
+# Languages used
+Back-end: Python3.6+
+Front-end: HTML, Javascript
+
+# How to install:
+1. Clone the repository into a folder
+2. Install requirements
+   1. ```pip install -r requirements.txt```
+
+# How to run server:
+ * Set up Python path
+   * Linux: ```export PYTHONPATH=${PYTHONPATH}:<your clone path>/truth_tree```
+ * Run web_server.py in the src folder and go to the ip address
+   * ```python3.6 web_server.py```
+   * Development Mode (Auto-Template Refresh) ```FLASK_APP=web_server_test.py FLASK_DEBUG=1 python3.6 -m flask run```
+ * Insert commands into Command to create the tree
+   * Try typing ```help```
+
+# How to run cli:
+ * Set up Python path
+   * Linux: ```export PYTHONPATH=${PYTHONPATH}:<your clone path>/truth_tree```
+ * Run cli.py in the src folder
+   * ```python3.6 cli.py```
+
+# How to run tests:
+ * Set up Python path
+   * Linux: ```export PYTHONPATH=${PYTHONPATH}:<your clone path>/truth_tree```
+ * Move into tests folder
+ * Run a tests file
+   * Example: ```python3.6 tests.py```
+
+# Current Supported Commands:
+* add_root_formula
+    * Add a "premise" to the truth tree
+        * Command to add a & b as a premise: 
+            * add_root_formula and(a,b)
+        * Command to add c | (d & e) as a premise:     
+            * add_root_formula or(c, and(d,e))
+* add_formula
+    * Add a formula to the current node
+        * Command to add a | b:
+            * add_formula or(a,b)
+        * Command to add ac -> bd:    
+            * add_formula if(ac,bd)
+* go_to
+    * Change the current node
+        * Command to set node 2 as current node:
+            * go_to 2
+        * Command to set node 1 as current node:
+            * go_to 1
+
+* delete_formula
+    * Delete a formula using the formula id
+        * Command to delete formula 1:
+            * delete_formula 1
+
+* undo
+    * Undo the last command
+        * Command to undo
+           * undo 
+
+* redo
+    * Redo a command
+        * Command to redo
+            * redo
+
+* close
+    * Close the current node using formula's in its ancestry
+        * Closing current node using formula 5 and 3:
+            * close 5 3
+
+* branch
+    * Branch on the current node using a formula
+        * Command to branch on current node using formula 1:
+            * branch 1
+
+* mark_parent
+    * Allow user to mark the parent of a formula
+        * Command to set formula 5 parent as 3
+            * mark_parent 5 1
+
+* checkmark
+    * Allow user to checkmark a formula after decomposing it
+        * Command to checkmark formula 3
+            * checkmark 3
+
+* mark_open
+    * Allow user to mark the current node as open
+        * Command to mark open
+            * Mark open
+
+* check_all_closed:
+    * Allow user to check if all branches have been closed properly
+        * Command to check
+            * check_all_closed
+
+* reset:
+    * Reset the tree. (WARNING will not be able to undo)
+        * Reset
+            * reset

2019/notation.md

@@ -0,0 +1,6 @@
+and(A, B) is equivalent to (A and B)
+or(A, B) is equivalent to (A or B)
+not(A) is equivalent ~A
+if(A, B) is equivalent to (A -> B)
+iff(A, B) is equivalent to (A <-> B)
+

2019/requirements.txt

@@ -0,0 +1,2 @@
+flask
+forseti

2019/src/Example/Example1.txt

@@ -0,0 +1,16 @@
+add_root_formula(if(K, not(K)))
+add_root_formula(not(not(K)))
+add_formula(K)
+mark_parent 3 2
+checkmark 2
+branch 1
+go_to 2
+add_formula(not(K))
+mark_parent 4 1
+close 4 3
+go_to 3
+add_formula(not(K))
+mark_parent 5 1
+close 5 3
+checkmark 1
+check_all_closed

2019/src/Example/Example2.txt

@@ -0,0 +1,13 @@
+add_root_formula(if(R, R))
+add_root_formula(not(R))
+branch 1
+go_to 2
+add_formula(not(R))
+mark_parent 3 1
+go_to 3
+add_formula R
+mark_parent 4 1
+checkmark 1
+close 4 2
+go_to 2
+mark_open