content/tools/sat-smt/prover9.md

+++ title = 'Prover9' subtitle = 'Theorem Prover' links = [ { title = "Homepage", url = "https://www.cs.unm.edu/~mccune/prover9/", icon = 'fa-solid fa-home' }, ] applications = ["Theorem Prover"] developers = [] licenses = [] inputs = [] interfaces = ["CLI"] maintenance = ["Actively Maintained"] draft = false date = 2025-08-21 +++

Prover9 is an automated theorem prover for first-order and equational logic, and Mace4 searches for finite models and counterexamples. Prover9 is the successor of the Otter prover.