{"library":"pyprover","title":"PyProver: Resolution Theorem Proving","description":"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.","language":"python","status":"active","last_verified":"Sat May 16","install":{"commands":["pip install pyprover"],"cli":null},"imports":["from pyprover import expr","from pyprover import proves","from pyprover import strict_proves","from pyprover import simplify","from pyprover import strict_simplify","from pyprover import ForAll","from pyprover import Exists","from pyprover import Eq","from pyprover import props","from pyprover import terms","from pyprover import *"],"auth":{"required":false,"env_vars":[]},"quickstart":{"code":"from pyprover import expr, proves, ForAll\n\n# Define some propositions/predicates and terms\nF, G = expr('F'), expr('G')\nx, y = expr('x'), expr('y')\n\n# Construct formulas\nformula1 = expr('A & B')\nformula2 = ForAll(x, F(x) >> G(x))\n\n# Example of a simple proof: Modus Ponens\ngivens = [expr('P >> Q'), expr('P')]\nconclusion = expr('Q')\n\nis_proven = proves(givens, conclusion)\nprint(f\"Does {givens} prove {conclusion}? {is_proven}\")\n\n# Example with quantifiers\ngivens_quant = [ForAll(x, F(x) >> G(x)), F(x)] # Note: F(x) here acts as an instance for some x\nconclusion_quant = G(x)\n\nis_proven_quant = proves(givens_quant, conclusion_quant)\nprint(f\"Does {givens_quant} prove {conclusion_quant}? {is_proven_quant}\")","lang":"python","description":"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.","tag":null,"tag_description":null,"last_tested":null,"results":[]},"compatibility":{"tag":null,"tag_description":null,"last_tested":"2026-05-16","installed_version":"0.6.2","pypi_latest":"0.6.2","is_stale":false,"summary":{"python_range":"3.10–3.9","success_rate":100,"avg_install_s":1.7,"avg_import_s":0.55,"wheel_type":"wheel"},"results":[{"runtime":"python:3.10-alpine","python_version":"3.10","os_libc":"alpine (musl)","variant":"pyprover","exit_code":0,"wheel_type":"wheel","failure_reason":null,"import_side_effects":"broken","install_time_s":null,"import_time_s":0.42,"mem_mb":11.7,"disk_size":"19.1M"},{"runtime":"python:3.10-slim","python_version":"3.10","os_libc":"slim (glibc)","variant":"pyprover","exit_code":0,"wheel_type":"wheel","failure_reason":null,"import_side_effects":"broken","install_time_s":1.8,"import_time_s":0.31,"mem_mb":11.7,"disk_size":"20M"},{"runtime":"python:3.11-alpine","python_version":"3.11","os_libc":"alpine (musl)","variant":"pyprover","exit_code":0,"wheel_type":"wheel","failure_reason":null,"import_side_effects":"broken","install_time_s":null,"import_time_s":0.64,"mem_mb":12.8,"disk_size":"21.3M"},{"runtime":"python:3.11-slim","python_version":"3.11","os_libc":"slim (glibc)","variant":"pyprover","exit_code":0,"wheel_type":"wheel","failure_reason":null,"import_side_effects":"broken","install_time_s":1.8,"import_time_s":0.5,"mem_mb":12.8,"disk_size":"22M"},{"runtime":"python:3.12-alpine","python_version":"3.12","os_libc":"alpine (musl)","variant":"pyprover","exit_code":0,"wheel_type":"wheel","failure_reason":null,"import_side_effects":"broken","install_time_s":null,"import_time_s":0.75,"mem_mb":12.7,"disk_size":"13.1M"},{"runtime":"python:3.12-slim","python_version":"3.12","os_libc":"slim (glibc)","variant":"pyprover","exit_code":0,"wheel_type":"wheel","failure_reason":null,"import_side_effects":"broken","install_time_s":1.6,"import_time_s":0.68,"mem_mb":12.6,"disk_size":"14M"},{"runtime":"python:3.13-alpine","python_version":"3.13","os_libc":"alpine (musl)","variant":"pyprover","exit_code":0,"wheel_type":"wheel","failure_reason":null,"import_side_effects":"broken","install_time_s":null,"import_time_s":0.78,"mem_mb":12.7,"disk_size":"12.9M"},{"runtime":"python:3.13-slim","python_version":"3.13","os_libc":"slim (glibc)","variant":"pyprover","exit_code":0,"wheel_type":"wheel","failure_reason":null,"import_side_effects":"broken","install_time_s":1.5,"import_time_s":0.7,"mem_mb":12.7,"disk_size":"13M"},{"runtime":"python:3.9-alpine","python_version":"3.9","os_libc":"alpine (musl)","variant":"pyprover","exit_code":0,"wheel_type":"wheel","failure_reason":null,"import_side_effects":"broken","install_time_s":null,"import_time_s":0.39,"mem_mb":11.7,"disk_size":"18.6M"},{"runtime":"python:3.9-slim","python_version":"3.9","os_libc":"slim (glibc)","variant":"pyprover","exit_code":0,"wheel_type":"wheel","failure_reason":null,"import_side_effects":"broken","install_time_s":1.8,"import_time_s":0.3,"mem_mb":11.7,"disk_size":"19M"}]}}