PyProver: Resolution Theorem Proving

0.6.2 · active · verified Mon Apr 13

PyProver is a resolution theorem prover for first-order predicate logic, implemented in pure Python. It is written in Coconut, which compiles to universal Python, ensuring compatibility across various Python versions. The latest version is 0.6.2, released in March 2022. The project is currently in an alpha development stage and has an infrequent release cadence.

Warnings

gotcha The library is currently in 'Development Status :: 3 - Alpha'. This means the API might change in future versions without strict adherence to semantic versioning, and it may not be suitable for production environments requiring high stability.
Fix: Be aware of potential API changes and thoroughly test your code when upgrading versions. Consider the project's maturity level for your application's requirements.
gotcha When using the `expr` function to parse formulas, propositions and predicates must start with a capital letter (e.g., `P`, `Q`, `F(x)`), while constants, variables, and functions must start with a lowercase letter (e.g., `x`, `y`, `f(a)`).
Fix: Ensure correct casing for symbols when defining formulas via `expr` to avoid parsing errors.
gotcha While `from pyprover import *` is demonstrated for interactive use, it is generally recommended to import specific functions or classes (e.g., `from pyprover import proves, expr`) in Python files to prevent polluting the global namespace and improve code clarity.
Fix: Prefer explicit imports for better code organization and to avoid name collisions.
gotcha The last release (v0.6.2) was on March 2, 2022. This indicates that the project may not be actively maintained or updated, which could lead to a lack of new features, bug fixes, or compatibility updates for newer Python versions.
Fix: Users should consider the implications of an inactive project for long-term usage and support. Check the GitHub repository for recent commits or issues before relying heavily on it.

Install

pip install pyprover Install with pip

Imports

expr
```
from pyprover import expr
```
Used for parsing formulas from strings.
proves
```
from pyprover import proves
```
Determines if a conclusion can be derived from a set of givens.
strict_proves
```
from pyprover import strict_proves
```
Strict version of 'proves' without implicit assumptions.
simplify
```
from pyprover import simplify
```
Simplifies an expression, implicitly assuming something exists.
strict_simplify
```
from pyprover import strict_simplify
```
Strict simplification without implicit assumptions.
ForAll
```
from pyprover import ForAll
```
Represents the universal quantifier.
Exists
```
from pyprover import Exists
```
Represents the existential quantifier.
Eq
```
from pyprover import Eq
```
Represents equality.
props
```
from pyprover import props
```
Creates multiple propositions/predicates by name.
terms
```
from pyprover import terms
```
Creates multiple constants/variables/functions by name.
all_imports
```
from pyprover import *
```
While convenient for interactive use, it's recommended to import specific symbols in Python files to avoid global namespace pollution.

Quickstart

This quickstart demonstrates how to define formulas using the `expr` function and construct proofs using the `proves` function. It includes examples for propositional and first-order logic.

from pyprover import expr, proves, ForAll

# Define some propositions/predicates and terms
F, G = expr('F'), expr('G')
x, y = expr('x'), expr('y')

# Construct formulas
formula1 = expr('A & B')
formula2 = ForAll(x, F(x) >> G(x))

# Example of a simple proof: Modus Ponens
givens = [expr('P >> Q'), expr('P')]
conclusion = expr('Q')

is_proven = proves(givens, conclusion)
print(f"Does {givens} prove {conclusion}? {is_proven}")

# Example with quantifiers
givens_quant = [ForAll(x, F(x) >> G(x)), F(x)] # Note: F(x) here acts as an instance for some x
conclusion_quant = G(x)

is_proven_quant = proves(givens_quant, conclusion_quant)
print(f"Does {givens_quant} prove {conclusion_quant}? {is_proven_quant}")

view raw JSON →