Prover9 and Mace4
Otterの後継にあたるTheorem Prover.
Otterは触ったことあるけど,これはないや.
日本語だとどっちが正しいのだろう.定理証明機?定理証明器?定理証明システム?
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.