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