A heuristic procedure for proving inequalities
Switch branches/tags
Nothing to show
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Failed to load latest commit information.


The Polya Inequality Prover

Authors: Jeremy Avigad, Robert Y. Lewis, Cody Roux

Polya is a system designed to support interactive theorem proving by verifying the kinds of inequalities that arise in ordinary mathematical arguments. The method is described in the paper "A heuristic prover for real inequalities," available online. The version of the system described in the paper is tagged "v0.2".

The system is released under the Apache 2.0 license. It is still an experimental prototype, and feedback is very welcome.

For instructions on setting up and using Polya, see the file 'INSTALL.md'.

Once Polya is installed, you can use it directly in the Python 2.7 interactive mode. Start Python:


and at the prompt type

from polya import *

at which point you can enter the command


to see which external packages are present.

There are a tutorial and sample problems in the folder 'examples'. See the 'README.md' in that folder for more information.

For benchmark comparisons, see 'examples/results.md' and the data in the folder 'examples/other_systems'.

Polya can now take SMTLIB input: https://github.com/rlewis1988/smtlib2polya