* curry

Initial commit of curry

* curry

Update

* curry

Begin adding operations on premises

* curry

This commit has lots of refactoring. It made more sense for all of the
different things happening in the proof file to be separated into
different modules. There is now a goal, premise, and show modules.

* curry

Clean up files that should not have been committed.

* curry

Implement and test disjunction-elimination

* curry

The next step in this process. For some reason serializing formulas is broken

* curry

Add the beginning of a major mode for writing proofs and continue to
reorganize code to make it easier to work with

* curry

There are a bunch of changes here.

1.  There was a bug in logos.formula/to-sting in displaying
disjunctions that is now fixed

2. We added several new routes
    a. One to clear the current proof
    b. One to evaluate a string representing a list  of commands

3. There was a bug with a proof's ability to close things off
properly. There are two tests that record the fixed behavior.

* curry

Update the tests so that they actually run and pass.

Update the theorem declaration syntax so that it includes a title for
the theorem.

* curry

Add support for universals

* curry

Add support for existential

* curry

Make formulas print even prettier

* curry

Revert changes to make formula printing a cleaner. It didn't work in
context. Existential proofs needed to be treated specially. And we
neded variables to also be predicates. This is a higher order logic

* curry

This has a lot of changes. It introduces a UI and formula
parsing. I'll write more about it in the PR

* curry

Update the todos

* curry

Some small cleanups after trying to get everything to work

* read-formula

Add the ability to start a formula with the same as it's serialized form

* read-formula

Add the ability to start a formula with the same as it's serialized form

* read-formula

This commit adds functionality that allows the user to enter a formula
into the app the same way that formula would be displayed by the app.

* read-formula

This commit adds the ability to parse a string that looks like a
formula structure as well as a formula as it's serialized.

* clean-up-todos

This PR cleans up the todos file. In particular it renames it and adds
ids to track the todos on git

* F616D54A-BA0D-48E0-BAE2-269A4113D0AC

This PR removes any reliance on state in the backend of the
application itself. All information about the proof is encoded in a
string that is passed to the front end, when a command is to be
performed, that same string is passed back so that backend knows what
to operate on. This should make it much easier to have concurrent
users on the system. It's also just much cleaner

* F999DB06-AA05-4D2C-BAE8-0BF885BC83F7

First attempt at using modals for any premise operations

* develop

Update README and dependencies

* F999DB06-AA05-4D2C-BAE8-0BF885BC83F7

This PR updates the way that premise selection is handled for premise
operations. Before this PR all premise selection was in the view of
hte proof. Now, all premise operations open up a modal. This modal
allows for premise selection and in cases where necessary, the
specification of variables to instantiate.

* D01BD36C-E447-4215-BB22-30C9857279D4

This PR adds support for `assert`. At any point in a proof a new
assertion can be made. This assertion is taken as a new goal. Once it
is proved the asserted formula can then be used as a premise.

Three tests have been added for this functionality. The update broke a
couple other tests which required updates.

This ended up also fixing some of the bugs that are in the todo file.

* 3FEC10EC-1326-405B-BD3E-79EEAC3B687E

This PR accomplishes two things:
 1. All formulas that are sent to be displayed by the front-end are
 pretty printed.

 2. A bug with second order variables was fixed. It used to be that
 instantiating second order variables would not actually generate an
 atomic-predicate, but would generate a constant. This PR fixes that.

* 5012FF0F-92F4-4989-91F9-E7D53DA8B788

This commit adds tooltips to the proof operation buttons

* 5012FF0F-92F4-4989-91F9-E7D53DA8B788

Update quantifier rules to also be able to substitute formulas

* 5012FF0F-92F4-4989-91F9-E7D53DA8B788

Tests also had to be updated

* 5012FF0F-92F4-4989-91F9-E7D53DA8B788 Add Tutorial

This commit adds a tutorial page to logos. The tutorial is designed
for someone who has some familiarity with philosophical logic to
acquaint themselves to the tool.

I couldn't help myself and added a more formal section on the
mathematical specification of formulas and the consequence relation.

It should be noted that the emacs plugin for this is now completely
broken but it could be fixed at some point.

Finally, I found a bug in disjunction-elimination that has been
fixed. The bug was a todo item, so that has also been closed.

* develop

I found a quick and easy way to fix the navbar so I'm adding it here.

* develop

Update the todos -- it's a little scope creep but I think there may be
a security issue

* hotfix-existential-elimination-broken

There was a problem with existential elimination. We weren't treating
the variable substitution and reading the same way as other
substitutional rules.

* develop

This has already been done at some point

* 0DBDB8EE-7742-4237-B9DA-D52E7F9E042D: Add Theorems Pane

This commit primarily adds the theorem pane. This pane is toggle-able
with a "show/hide" span. It displays the theorem name, the theorem
formula, and the justification for that theorem.

In passing

1. Fixes a bug with formula-gather
2. Adds more to the scope of v1, but most of the additions are bugfixes.

* 3A6163AC-CEDF-4E5E-A6CD-DCE5FF1424F9: Add A Format Button

This commit adds a button on the start proof page that formats the
current formula. There are a few problems with this button:

1. It does not use the standard events loop and instead synchronously
calls to the backend
2. It doesn't offer much help to the user other than formatting a
wff.

* 3A6163AC-CEDF-4E5E-A6CD-DCE5FF1424F9: Add error handling

This commit adds error handling for the format button and brings back
the error modal that somehow got deleted.

* develop: Update TODOs

Small update on todos to prioritize the work to be done.

* F114BD39-B6D9-4E7E-9AA7-3513D0637583: Replace Dangerous Read Strings

This PR replaces any occurrence of read-string that occurrs in the
context of reading a formula with read-formula-string which is a safe
way of parsing a formula string. Additionally it removes all instances
of read-string from the premises file and replaces them with
Integer/parseInt. Finally any reading of an internal edn
representation of a structure has been replaced with edn/read-string.

* DB61BAE3-60D9-46AA-8AC8-33540BE98631: Error on Wrong Premise Number

This PR adds an error message when the wrong number of premises is
passed to for a rule. The error is surfaced to the user.

It also adds an environment variable for what the hostname is. This
should make releasing much quicker.

* HOTFIX: Bad envvars

I chose a bad envvar for the umls server. This commit fixes that

* D959DCB7-B4B4-4C17-82C3-7BCA4A3C2E0F: Logging

Initial commit of the logging framework.

* 013A20CF-E0DC-47DA-9198-F146E37A0F49: Support equality and fix bug

This PR does two things:

1. It adds support for an equality predicate "!equals"

2. It fixes a bug where the theorem name a user inputs could not have
any spaces in it.

* D959DCB7-B4B4-4C17-82C3-7BCA4A3C2E0F: Logging

This PR ensures that logging works as expected. There are two logging
statements which are printed out stdout and written to disk. The first
records when the service was started. The second records anytime that
someone starts a proof.

* 2C2AE56C-D36F-43F8-A1F2-7E3AB49D0FBB: Deployment and README

This is the last real code commit for v1 of logos. It includes an
updated readme, dockerfile, and a script for running logos. The only
thing left is to set up CI to run tests on merge to develop and main.

* Create clojure.yml

* develop: Finish V1

Finish up the todos on V1 and bump the version

* develop: Update README

Fix issue with the README and add a build badge

* develop: Last Fix

One last README fix

* Premise Support

Make it possible to add premises to a proof context.

* Complex terms one 

** Update dockerfile and suport term substituion

** Use Dockerfiles in compose

This is better because we can copy files into the containers instead
of mounting volumes and writing out a bunch of files