Prover9 and Mace4

research

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.

http://www.cs.unm.edu/~mccune/mace4/