eprover ☆
« Back to VersTracker
Description:
Theorem prover for full first-order logic with equality
Type: Formula  |  Latest Version: 3.2@0  |  Tracked Since: Dec 17, 2025
Links: Homepage  |  formulae.brew.sh
Category: Developer tools
Tags: theorem-prover logic formal-verification automated-reasoning research
Install: brew install eprover
About:
EProver is a high-performance automated theorem prover for full first-order logic with equality. It implements the resolution calculus and is designed to prove theorems from a set of axioms and formulas. Its main value proposition is its speed and robustness in solving complex logical problems, making it a key tool in automated reasoning research.
Key Features:
  • High-performance resolution-based proving engine
  • Supports the TPTP (Thousands of Problems for Theorem Provers) format
  • Implements equality reasoning and various inference rules
  • Capable of producing formal proof objects
  • Includes related tools like EGround for finding ground instances
Use Cases:
  • Automated verification of software and hardware correctness
  • Research in artificial intelligence and automated reasoning
  • Solving mathematical problems expressed in first-order logic
  • Validating logical consistency of knowledge bases
Alternatives:
  • Vampire – Another leading high-performance first-order theorem prover, often competing with E in international competitions.
  • Z3 – A theorem prover from Microsoft Research that supports SMT (Satisfiability Modulo Theories), handling more expressive logics than pure first-order.
License: GPL-2.0-or-later OR LGPL-2.1-or-later
Bottles available for: arm64_tahoe, arm64_sequoia, arm64_sonoma, arm64_ventura, sonoma, ventura, arm64_linux, x86_64_linux
Version History
Detected Version Rev Change Commit
Sep 13, 2025 2:15pm 0 VERSION_BUMP e3c3410f
Sep 13, 2024 3:12am 0 VERSION_BUMP 13c74419
Nov 27, 2023 1:29am 0 VERSION_BUMP 102ced29
Nov 26, 2023 5:15pm 0 VERSION_BUMP 623d432d
« Back to VersTracker  |  Browse Packages  |  About