Implementation of higher-order logic in Python.
See README file in the
Unit tests for the backend are located in files of the form
Run all unit tests on Windows:
python -m unittest discover -p *_test.py
python3 -m unittest */tests/*_test.py
This project requires Python 3.5 or greater and npm:
Required packages are listed in requirements.txt. To install required packages in the global environment, you can use:
python -m pip install -r requirements.txt
Depending on your system, may need to replace python by python3 or python3.x.
To avoid conflicts between projects that require different versions of packages,
we recommend installing Python packages in an isolated environment, e.g.
when using the
bash shell, in the repository root directory do:
$ python3 -m venv ENV # Run python3.5 or above. $ source ENV/bin/activate # Sets up "python" to be your python3. $ python -m pip install -r requirements.txt $ python app.py # Runs the backend server on localhost:5000
In this same shell you can restore your previous environment later with
The user interface is built using Vue, in the
./app folder. To set up and
run the user interface server, in a different terminal
./app and use
npm install followed by
npm run serve.
In your browser the user interface is at page
To see statistics for the search functionality on a collection of lemmas, use:
python -m server.collect_stat
kernel: kernel for higher-order logic.
type: datatype for HOL types.
term: datatype for HOL terms.
thm: datatype for HOL theorems, including list of basic derivations.
proof: linear representation of a proof, consisting of a list of instructions to the kernel.
macro: macros as user-defined proof methods.
theory: theory state, containing signature for types and constants, and list of axioms and theorems.
extension: types of extensions to a theory.
report: statistics and debugging information for checking a theory extension.
logic: base logic and standard automation.
data: common data types.
syntax: parsing and printing.
server: toplevel functions.
app: web application.
__init__.py: main server program.
library: main library of theories.