Skip to content

Commit

Permalink
Updated README again.
Browse files Browse the repository at this point in the history
  • Loading branch information
Joshua Crotts committed Aug 9, 2021
1 parent 234517a commit bf58af1
Showing 1 changed file with 17 additions and 16 deletions.
33 changes: 17 additions & 16 deletions README.md
Original file line number Diff line number Diff line change
@@ -1,16 +1,16 @@
<h1><center>Formal Logic Aiding Tutor</center></h1>
<h1><p align="center">Formal Logic Aiding Tutor</p></h1>

<h3>Introduction</h3>
<h2>Introduction</h2>
FLAT (the Formal Logic Aiding Tutor) is an extension to LLAT (the Logic Learning Assistant Tool) that aims to improve the overall pedagogical value. That is, rather than being only a brute-force solver, we have included new features that help students better understand the logic.

<h3>Features</h3>
<h2>Features</h2>
FLAT features several algorithms, or subfeatures, for students to use. These include
- Natural Deduction Prover (no conditional or indirect proofs)
- Truth Tree (semantic tableaux) Generator
- Argument Validity via Truth Tree Determiner
- Open/Closed/Ground Sentence Determiners
- Bound/Free Variable Detectors
- Logical Relationship Determiners
- Logical Relationship Determiners
- Truth Table Generator
- Vacuous Quantifier Detector
- Random Logic Formula Generator
Expand All @@ -21,14 +21,15 @@ FLAT features several algorithms, or subfeatures, for students to use. These inc

We also allow the user to change the UI color scheme and language. Be aware, though, that language changes, along with PDF generation, require an internet connection.

In the settings menu, there is an __Advanced__ section. For the beginning student, this menu should be avoided. If, however, you wish to raise the limits that the program enforces for algorithm timeouts, this is where they are located.
In the settings menu, there is an __Advanced__ section. For the beginning student, this menu should be avoided. If, however, you wish to raise the limits that the program enforces for algorithm timeouts, this is where they are located.

<h3>Using FLAT</h3>
To use FLAT:
1. Open the application and type a well-formed formula in propositional or first-order predicate logic in the bottom text input field.

_Note:_ Make sure to use parentheses around the wffs and to avoid parentheses when typing predicates (i.e., use Pxyz and not P(x, y, z)). Unary operators such as negation do not use parentheses. All binary operators require parentheses. In other words, there is __no implicit precedence of operators!__
2. Click the Solve button. If an error pops up, read it, then re-enter your wff making sure to correct any mistakes. After this, the top three drop-downs should be populated with algorithms appropriate for your input.
<h2>Using FLAT</h2>
To use FLAT:

1. Open the application and type a well-formed formula in propositional or first-order predicate logic in the bottom text input field.

_Note:_ Make sure to use parentheses around the wffs and to avoid parentheses when typing predicates (i.e., use Pxyz and not P(x, y, z)). Unary operators such as negation do not use parentheses. All binary operators require parentheses. In other words, there is __no implicit precedence of operators!__
2. Click the Solve button. If an error pops up, read it, then re-enter your wff making sure to correct any mistakes. After this, the top three drop-downs should be populated with algorithms appropriate for your input.
3. Now, click the algorithm you want to try. Then, click the Apply button. Assuming everything is done correctly, the buttons below the three drop-downs will light up (again, depending on which algorithm you used). Click these to investigate the output.
4. Trees are draggable and adjustable. To adjust a subtree, just click and drag it around. To zoom in and out, use the mouse wheel.

Expand All @@ -38,13 +39,13 @@ __Rules/Axioms__ is the other viewable pane on the right-hand side which display

__Symbols__ in the left-hand side are swappable. If, for instance, you use a different symbol than the ones displayed, you can change it to your liking. Simply right-click the symbol and a drop-down will appear, allowing you to select one of several alternatives.

<h3>Rebuilding FLAT</h3>
We built FLAT using the Maven architecture and IntelliJ IDE. We have, however, designed the project to be IDE-agnostic. Though, because we use JavaFX without modules, Java 8 is the only supported version. We used Amazon Corretto's JRE8/JDK8, so it's recommended that you do as well.
<h2>Rebuilding FLAT</h2>
We built FLAT using the Maven architecture and IntelliJ IDE. We have, however, designed the project to be IDE-agnostic. Though, because we use JavaFX without modules, Java 8 is the only supported version. We used Amazon Corretto's JRE8/JDK8, so it's recommended that you do as well.

To rebuild the project, clone the repository to your computer and open it in whichever IDE you wish. Assuming it detects Maven projects correctly (Eclipse, NetBeans, and IntelliJ work), it should open and compile correctly.
To rebuild the project, clone the repository to your computer and open it in whichever IDE you wish. Assuming it detects Maven projects correctly (Eclipse, NetBeans, and IntelliJ work), it should open and compile correctly.

<h3>References</h3>
To cite this project, use the following paper citation: <to put here...>
<h2>References</h2>
To cite this project, use the following paper citation: to put here...

PDF generation uses the following remote API: https://github.com/YtoTech/latex-on-http

Expand Down

0 comments on commit bf58af1

Please sign in to comment.