holpy

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:

https://www.python.org/download/releases/3.0/:

https://www.npmjs.com/

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.

  • nat: natural numbers.
  • function: functions.
  • list: lists.
  • set: sets.
  • real: real numbers.

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

  • __init__.py: main server program.

• library: main library of theories.