Implementation of higher-order logic in Python.
See README file in the integral
directory.
This project requires Python 3.5 and npm:
https://www.python.org/download/releases/3.0/
Required packages are listed in requirements.txt. To install required packages, use (depending on your system, may need to replace python by python3 or python3.x):
python -m pip install -r requirements.txt
The user interface is built using Vue, in the ./app folder. To start,
change to ./app and use npm install
followed by npm run serve
,
then start the server (in the root directory) using python app.py
,
and go to page localhost:8080
.
To see statistics for the search functionality on a collection of lemmas, use:
python -m server.collect_stat
Unit tests for the backend are located in files of the form */tests/*_test.py
.
-
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.