Athena v1.5.4

This releases adds higher-order logic functionality to Athena, enabling quantification over functions.

• Sorts of the form (Fun S_1 ... S_n T) now accepted

• Arbitrary app terms accepted now

• Auto-adding lifted symbol versions

• Handled unary app cases

• Restored infix_parser.sml

• Overloaded and input-expanded symbols now also do term lifting as needed

• uspec now accepts higher-order values as the second argument

• Explicit app's of lifted symbols are now auto-simplifed in AT.makeApp1 rather than the evaluator level

• Added primitive method functor-identity

• Examples in sf/code/hol4.ath working

• Proper 'app' sort checking for unary, binary, and general applications

• Checking in lib/basic/hol_examples.ath

• Implemented promotion of anonymous lambdas

Athena v1.4.3

V1.4.3

Athena v1.4.2

V1.4.2 (#8)

* fix: vamp_proof_line assigned vampire's output in the case of refutation

* Makefile clean recipe doesn't delete all contents in build directory; only athena-specific files

* bump minor version

* fix vamp_proof_line

Athena v1.4.1 (FPMICS)

This release is provided to be fully compatible with examples and exercises from the book Fundamental Proof Methods in Computer Science (FPMICS) by Konstantine Arkoudas (@konstantine4096) and David Musser.

Some minor changes are also included:

• Make recipes are used for building and testing Athena
• Some additional utility scripts are provided for running Athena and installing external ATPs, SAT solvers, and ML compilers
• Thorough code comments by @konstantine4096
• Some improvements to the regression test suite
• CI/CD

Note: The Windows release is a copy of the distribution of Athena 1.4.0 that used to be hosted on Proof Central. The purpose of this release (1.4.1 FPMICS) is to provide a set of Athena distributions that are fully compatible with all examples & exercises in the book. It is in the spirit of this goal of preservation to provide distributions for the same platforms as Athena's previous home. Future releases may not contain Windows distributions and it is recommended that Windows users utilize WSL in conjunction with athena-linux, instead.