prover9 mit Homebrew installieren

Projektlinks

• Homepage

Befehle und Aliase

• mace4
• prover9

Projektgeschichte

Prover9 succeeded McCune's Otter prover and continued the Argonne automated-deduction line associated with Otter, EQP, Mace4, and LADR. The official 2009 manual presents Prover9 as the current Prover9/Mace4 release line at that time, while the 2026 site describes LADR-2026 as a backward-compatible modernization by Jeffrey P. Machado and Larry Lesyna.

Adoptionsgeschichte

The package has remained useful enough for Unix package managers to carry the 2009-11A release: Homebrew lists a `prover9` formula for macOS and Linux, and the input metadata also records Nix packaging. The 2026 project site recommends LADR-2026 for Prover9 and Mace4 users while preserving old input compatibility.

Wie es verwendet wird

Command-line users provide one or more Prover9 input files containing formula lists, clauses, goals, options, and related objects; the manual's basic example runs `prover9 -f subset_trans.in > subset_trans.out`. Mace4 is commonly used alongside Prover9 to search for finite counterexamples before or during proof search.

Warum Paket-Nerds sich dafür interessieren

For package-manager users, Prover9 is a small but historically important automated-reasoning tool: it exposes classic theorem-proving workflows as CLI programs, ships with related utilities such as Mace4 and Prooftrans, and represents the long-lived LADR codebase in reproducible Unix package collections.

Zeitleiste

• 2009: Prover9/Mace4 2009-11A manual and examples are published as the current older release.
• 2026-03: The UNM page announces LADR-2026 as a substantially revised, backward-compatible Prover9 and Mace4 version.
• 2026-05: The official GitHub repository lists LADR 2026-5B as the latest release.

Related projects

• Mace4 searches for finite models and counterexamples for the same kinds of first-order and equational statements Prover9 accepts.
• Otter is the earlier theorem prover that Prover9 succeeded.
• Prooftrans is bundled with Prover9 to transform proofs into alternate forms, including more detailed or XML output.

Quellen

• https://formulae.brew.sh/formula/prover9
• https://prover9.org/
• https://prover9.org/manual-2026/
• https://www.cs.unm.edu/~mccune/prover9/
• https://www.cs.unm.edu/~mccune/prover9/manual/2009-11A/input.html
• input_path source_facts.package-manager