The Equational Theorem Prover E

A simple repackaging of the E automated theorem prover for ease of installation and execution from python. All rights and licensing are up to the eprover authors. The higher order extension is enabled.

Supplies a universal binary built using Cosmopolitan libc. This should work on linux, windows, mac. x86_64 or aarch64.

Installation

git clone https://github.com/philzook58/pyeprover
cd pyeprover
python3 -m pip install -e .

or

pip install git+https://github.com/philzook58/pyeprover

import eprover
eprover.binpath()
eprover.run(["/tmp/test.p"], capture_output=True) # same arguments as subprocess.run

You can also run it as a module command

python -m eprover /tmp/test.p