hermetique / holpy Goto Github PK

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/

https://www.npmjs.com/

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.

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