athenafoundation/athena

Athena is a modern, practical language for proof engineering & natural deduction.

athena's Issues

Calls to Vampire ATP always fail

For example:

module AutomatedProofExample {
      (print "-------Automated Proof Example----------")
      declare A,B,C,D: Boolean
      assume h1 := (A & B)
      assume h2 := (~C ==> ~B)
      (!derive-from C [h1 h2] |{'atp := 'vampire}|)
}

This will fail, yet it is clearly provable. Replacing 'vampire with 'spass works.

Checking the vampire output logs, even when Vampire reports a successful proof, Athena reports that Vampire discovered a refutation

Refactor Regression Tests to Remove External Deps & Other Failure Cases

What is wrong
Currently, regression tests rely on both Minisat and SPASS. The regression test suite thus reports 8 total failures when run on a freshly cloned repository:
2 reported failures are from book code examples that are meant to raise errors.
1 reported failure is due to proof search failing when using a build generated by SML/NJ. This failure is not due to problems with Athena, rather, the non-deterministic nature of proof search procedures, possible timeouts, etc.
1 reported failure is due to missing the minisat_out.txt file in the ATHENA_HOME directory.
The other four failures are due to external calls to either Minisat or SPASS, which fail when they have not been installed.

How to fix
First, we will remove the intentionally incorrect code examples since they are meant for pedagogical purposes. Later, we might add to the python regression script an ability to expect an error from the Athena proof-checking.

Next, we will add to the regression testing script(s) an initial procedure that checks for Minisat and SPASS in the user's path. If Minisat is present, the original tests will be used, otherwise, it will trigger equivalent tests that use an Athena-native sat procedure. If SPASS is absent, tests that rely on SPASS will simply be skipped.

Syntax highlighting

Add syntax highlighting support for popular IDEs (VSCode, Atom, IntelliJ).

Support for language server protocol should also be developed.

Regression testing does not exit

When running regression tests using the provided tests:

python3 tests/regression/regressionTest.py athena

Athena does not quit after loading a test. It looks like the python script tests/regression/regressionTest.py just tries to load each file like:

         cmd = athena_executable + ' ' + input_file + ' quit > ' + res_file

But the quit command line argument doesn't do anything when built with MLTON.
This will halt on the first test file loaded and will not continue.

Additionally having no Athena installation results in the regression testing passing with zero errors, which is not good. Reproducible by cloning on any machine that has no athena installation and running

python3 tests/regression/regressionTest.py
.
.
.
Total number of errors: 0, all output found in /path/to/regression_results.txt.

Sort Unification for Subsort Relations in Modules

Athena rejects the use of unifiable sorts constructed via subsorts when in the context of a module.

Below are two code snippets, identical except that the second code snippet defines the BTree and related code inside of a Tree module, while the first snippet is defined in the top level Athena context.

datatype (BTree T) :=
    null |
    (leaf T) |
    (root (BTree T) (BTree T))

domains Sort1, Sort2, Sort

subsorts (Sort1 Sort2) Sort

declare data1: Sort1
declare data2: Sort2

define tree1 := (leaf data1)
define tree2 := (leaf data2)
define tree := (root tree1 tree2)

module Tree {

  datatype (BTree T) :=
      null |
      (leaf T) |
      (root (BTree T) (BTree T))
  
  domains Sort1, Sort2, Sort
  
  subsorts (Sort1 Sort2) Sort
  
  declare data1: Sort1
  declare data2: Sort2
  
  define tree1 := (leaf data1)
  define tree2 := (leaf data2)
  define tree := (root tree1 tree2)
}

Example 1 runs without error, while evaluating example 2 will cause Athena to report the following problem:

Error: Unable to infer a sort for the term: 

(Tree.root (Tree.leaf Tree.data1)

           (Tree.leaf Tree.data2))

(Failed to unify the sorts Tree.Sort2 and Tree.Sort1.).