16 Star 16 Fork 6

Bohua Zhan / holpy

Create your Gitee Account
Explore and code with more than 8 million developers,Free private repositories !:)
Sign up
Clone or Download
Sync branch
Notice: Creating folder will generate an empty file .keep, because not support in Git


Implementation of higher-order logic in Python.

Verification of symbolic integration:

See README file in the integral directory.

Unit tests

Unit tests for the backend are located in files of the form */tests/*_test.py.

Run all unit tests on Windows:

python -m unittest discover -p *_test.py

On Linux:

python3 -m unittest */tests/*_test.py

Installation and usage:

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

$ deactivate

The user interface is built using Vue, in the ./app folder. To set up and run the user interface server, in a different terminal change to ./app and use npm install followed by npm run serve.

In your browser the user interface is at page localhost:8080.

To see statistics for the search functionality on a collection of lemmas, use:

python -m server.collect_stat

Directory structure:

  • 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.

    • matcher: matching of terms.
    • proofterm: tree-like representation of a proof. Used for convenient construction of proofs, and can be transformed to the linear representation.
    • conv: conversions.
    • logic: utilities and definition of standard macros for logic.
    • basic: functions for loading theories.
  • data: common data types.

  • syntax: parsing and printing.

    • operator: data for unary and binary operators.
    • infertype: type inference.
    • printer: printing functions.
    • parser: parsing functions, built using Lark parser.
  • server: toplevel functions.

    • server: definition and standard operations for proof states.
    • tactic: definition of tactics.
    • method: definition of methods.
  • app: web application.

  • library: main library of theories.


Implementation of higher-order logic in Python. expand collapse


No release




Load More
can not load any more


10d9f8b4 4838521 8bde8327 4838521