athenafoundation / athena Goto Github PK
View Code? Open in Web Editor NEWAthena is a modern, practical language for proof engineering & natural deduction.
License: Apache License 2.0
Athena is a modern, practical language for proof engineering & natural deduction.
License: Apache License 2.0
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
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.
Add syntax highlighting support for popular IDEs (VSCode, Atom, IntelliJ).
Support for language server protocol should also be developed.
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.
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.).
A declarative, efficient, and flexible JavaScript library for building user interfaces.
๐ Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. ๐๐๐
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google โค๏ธ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.