prover9 - Theorem Prover and Countermodel Generator

Property Value
Distribution Fedora Rawhide
Repository Fedora x86_64
Package name prover9
Package version 200911a
Package release 12.fc26
Package architecture x86_64
Package type rpm
Installed size 2.95 MB
Download size 526.87 KB
Official Mirror
This package provides the Prover9 resolution/paramodulation theorem prover
and the Mace4 countermodel generator.
Prover9 is an automated theorem prover for first-order and equational logic.
It is a successor of the Otter prover. Prover9 uses the inference techniques
of ordered resolution and paramodulation with literal selection.
The program Mace4 searches for finite structures satisfying first-order and
equational statements, the same kind of statement that Prover9 accepts. If
the statement is the denial of some conjecture, any structures found by
Mace4 are counterexamples to the conjecture.
Mace4 can be a valuable complement to Prover9, looking for counterexamples
before (or at the same time as) using Prover9 to search for a proof. It can
also be used to help debug input clauses and formulas for Prover9.


Package Version Architecture Repository
prover9 - - -


Name Value - - -
rtld(GNU_HASH) -


Name Value
prover9 = 200911a-12.fc26
prover9(x86-64) = 200911a-12.fc26


Type URL
Binary Package prover9-200911a-12.fc26.x86_64.rpm
Source Package prover9-200911a-12.fc26.src.rpm

Install Howto

Install prover9 rpm package:

# dnf install prover9




2017-02-11 - Fedora Release Engineering <> - 200911a-12
- Rebuilt for
2016-02-04 - Fedora Release Engineering <> - 200911a-11
- Rebuilt for
2015-07-27 - Bruno Wolff III <> - 200911a-10
- Fix format string warning
2015-06-18 - Fedora Release Engineering <> - 200911a-9
- Rebuilt for
2014-08-17 - Fedora Release Engineering <> - 200911a-8
- Rebuilt for
2014-06-07 - Fedora Release Engineering <> - 200911a-7
- Rebuilt for
2013-08-04 - Fedora Release Engineering <> - 200911a-6
- Rebuilt for
2013-02-14 - Fedora Release Engineering <> - 200911a-5
- Rebuilt for
2012-07-21 - Fedora Release Engineering <> - 200911a-4
- Rebuilt for
2012-01-14 - Fedora Release Engineering <> - 200911a-3
- Rebuilt for

See Also

Package Description
prover9-apps-200911a-12.fc26.x86_64.rpm LADR Deduction Library - Miscellaneous Applications
prover9-devel-200911a-12.fc26.i686.rpm LADR Deduction Library - Development Files
prover9-devel-200911a-12.fc26.x86_64.rpm LADR Deduction Library - Development Files
prover9-doc-200911a-12.fc26.x86_64.rpm LADR Deduction Library - Documentation
proxool-0.9.1-22.fc29.noarch.rpm Java connection pool library
proxool-javadoc-0.9.1-22.fc29.noarch.rpm Javadoc for proxool
proxychains-ng-4.13-2.fc30.x86_64.rpm Redirect connections through proxy servers
proxyfuzz-20110923-12.fc29.noarch.rpm Man-in-the-middle non-deterministic network fuzzer
proxysql-1.3.7-8.fc29.x86_64.rpm A high-performance MySQL proxy
proxytoys-1.0-12.fc29.noarch.rpm An implementation neutral API for creation of dynamic proxies
proxytoys-example-code-1.0-12.fc29.noarch.rpm ProxyToys Example Code
proxytoys-javadoc-1.0-12.fc29.noarch.rpm Javadoc for proxytoys
proxytoys-parent-1.0-12.fc29.noarch.rpm ProxyToys parent POM
proxytunnel-1.9.1-7.fc29.x86_64.rpm Tool to tunnel a connection through an standard HTTP(S) proxy
prozilla-2.0.4-18.fc22.x86_64.rpm Advanced Linux download manager