gym-saturation

gym-saturation: an OpenAI Gym environment for saturation provers - Published in JOSS (2022)

https://github.com/inpefess/gym-saturation

Repository

a collection of Gymnasium environments for saturation provers

README.rst

..
  Copyright 2021-2025 Boris Shminke

  Licensed under the Apache License, Version 2.0 (the "License");
  you may not use this file except in compliance with the License.
  You may obtain a copy of the License at

      https://www.apache.org/licenses/LICENSE-2.0

  Unless required by applicable law or agreed to in writing, software
  distributed under the License is distributed on an "AS IS" BASIS,
  WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
  See the License for the specific language governing permissions and
  limitations under the License.

|PyPI version|\ |Anaconda|\ |CircleCI|\ |Documentation Status|\ |codecov|\ |DOI|

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
==============

.. attention:: If you want to use ``VampireEnv`` you should have a
   Vampire binary on your machine. For example, download the
   latest `release
   `__.

   To use ``IProverEnv``, please download a stable iProver 
   `release
   `__ or build it from `this commit `__.

The best way to install this package is to use ``pip``:

.. code:: sh

   pip install gym-saturation

Another option is to use ``conda``:

.. code:: sh

   conda install -c conda-forge gym-saturation
   
One can also run it in a Docker container (pre-packed with
``vampire`` and ``iproveropt`` binaries):

.. code:: sh

   docker build -t gym-saturation https://github.com/inpefess/gym-saturation.git
   docker run --rm -p 8888:8888 --name gym-saturation -d gym-saturation

and navigate to ``__ in
your browser.

How to use
==========

One can use ``gym-saturation`` environments as any other Gymnasium environment:

.. code:: python

  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
      action = ...
      observation, reward, terminated, truncated, info = env.step(str(action))
  env.close()

Have a look at the basic `tutorial `__.  

More Documentation
==================

More documentation can be found
`here `__.

Related Projects
=================

Other projects using RL-guidance for ATPs include:

* `TRAIL `__
* `FLoP `__ (see `the paper `__ for more details)
* `lazyCoP `__ (see `the paper `__ for more details)

Other projects not using RL per se, but iterating a supervised
learning procedure instead:

* ENIGMA (several repos, e.g. `this one
  `__ for
  iProver; see `the paper `__ for
  others)
* `Deepire `__

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 `__.

.. |PyPI version| image:: https://badge.fury.io/py/gym-saturation.svg
   :target: https://badge.fury.io/py/gym-saturation
.. |CircleCI| image:: https://circleci.com/gh/inpefess/gym-saturation.svg?style=svg
   :target: https://circleci.com/gh/inpefess/gym-saturation
.. |Documentation Status| image:: https://readthedocs.org/projects/gym-saturation/badge/?version=latest
   :target: https://gym-saturation.readthedocs.io/en/latest/?badge=latest
.. |codecov| image:: https://codecov.io/gh/inpefess/gym-saturation/branch/master/graph/badge.svg
   :target: https://codecov.io/gh/inpefess/gym-saturation
.. |DOI| image:: https://img.shields.io/badge/DOI-10.1007%2F978--3--031--43513--3__11-blue
   :target: https://doi.org/10.1007/978-3-031-43513-3_11
.. |Anaconda| image:: https://anaconda.org/conda-forge/gym-saturation/badges/version.svg
   :target: https://anaconda.org/conda-forge/gym-saturation

Owner

JOSS Publication

gym-saturation: an OpenAI Gym environment for saturation provers

Published

March 03, 2022

DOI

10.21105/joss.03849

Volume 7, Issue 71, Page 3849

Authors

Boris Shminke
Laboratoire J.A. Dieudonné, CNRS and Université Côte d'Azur, France

Editor

Viviane Pons

Tags

OpenAI Gym automated theorem prover saturation prover reinforcement learning

View PDF Review Thread Software Archive

GitHub Events

Committers

Last synced: 7 months ago

Issues and Pull Requests

Last synced: 6 months ago

Packages