Gymnasium environments for saturation provers
Project description
gym-saturation
gym-saturation is a collection of Gymnasium environments for reinforcement learning (RL) agents guiding saturation-style automated theorem provers (ATPs) based on the given clause algorithm.
There are two environments in gym-saturation following the same API: SaturationEnv: VampireEnv — for Vampire prover, and IProverEnv — for iProver.
gym-saturation can be interesting for RL practitioners willing to apply their experience to theorem proving without coding all the logic-related stuff themselves.
In particular, ATPs serving as gym-saturation backends incapsulate parsing the input formal language (usually, one of the TPTP (Thousands of Problems for Theorem Provers) library), transforming the input formulae to the clausal normal form, and logic inference using rules such as resolution and superposition.
How to Install
The best way to install this package is to use pip:
pip install gym-saturationAnother option is to use conda:
conda install -c conda-forge gym-saturationOne can also run it in a Docker container (pre-packed with vampire and iproveropt binaries):
docker build -t gym-saturation https://github.com/inpefess/gym-saturation.git
docker run -it --rm -p 8888:8888 gym-saturation jupyter-lab --ip=0.0.0.0 --port=8888How to use
One can use gym-saturation environments as any other Gymnasium environment:
import gym_saturation
import gymnasium
env = gymnasium.make("Vampire-v0") # or "iProver-v0"
# skip this line to use the default problem
env.set_task("a-TPTP-problem-filename")
observation, info = env.reset()
terminated, truncated = False, False
while not (terminated or truncated):
# apply policy (a random action here)
action = env.action_space.sample()
observation, reward, terminated, truncated, info = env.step(action)
env.close()Or have a look at the basic tutorial.
For a bit more comprehensive experiments, please see this project.
More Documentation
More documentation can be found here.
How to Contribute
Please follow the contribution guide while adhering to the code of conduct.
How to Cite
If you are writing a research paper and want to cite gym-saturation, please use the following DOI.
Release history Release notifications | RSS feed
Download files
Download the file for your platform. If you're not sure which to choose, learn more about installing packages.
Source Distribution
Built Distribution
Hashes for gym_saturation-0.11.6-py3-none-any.whl
| Algorithm | Hash digest | |
|---|---|---|
| SHA256 | 633109bd1d0603c55d5fd2b0a3aee699d98e66d92455b7da82d7dc5bd8c487e7 |
|
| MD5 | 803639475394f2a5539e108b1c233915 |
|
| BLAKE2b-256 | 2ba48a62c028086c7835583695b8856b5e0ca35cd8d3f0c1c44da0c00e6fe2a4 |
