How To Install eqp on Fedora 36
Introduction
In this tutorial we learn how to install eqp on Fedora 36.
What is eqp
EQP is an automated theorem proving program for first-order equational logic. Its strengths are good implementations of associative-commutative unification and matching, a variety of strategies for equational reasoning, and fast search. It seems to perform well on many problems about lattice-like structures. EQP is not a stable and polished production theorem prover like Otter or Prover9. Since it has obtained several interesting results, it was decided to make it available (including the source code) to everyone, with no restrictions (and of course no warranty either). EQP’s documentation is not great, but if you already know Otter, you probably will not have great difficulty in learning to use EQP. In the early 1930’s, it was postulated that every Robbin’s Algebra, (named after Herbert Ellis Robbins), must also be a Boolean Algebra. Many human mathematicians attempted to find a proof, or a counter-example of this conjecture, but failed. The EQP automated theorem prover (and its author William McCune) made history by providing the first known proof in 1996. The EQP input files for proving Robbin’s Conjecture can be found in the package documentation directory /usr/share/doc/eqp-09e/examples/robbins/
We can use yum or dnf to install eqp on Fedora 36. In this tutorial we discuss both methods but you only need to choose one of method to install eqp.
Install eqp on Fedora 36 Using dnf
Update yum database with dnf using the following command.
sudo dnf makecache --refresh
After updating yum database, We can install eqp using dnf by running the following command:
sudo dnf -y install eqp
Install eqp on Fedora 36 Using yum
Update yum database with yum using the following command.
sudo yum makecache --refresh
After updating yum database, We can install eqp using yum by running the following command:
sudo yum -y install eqp
How To Uninstall eqp on Fedora 36
To uninstall only the eqp package we can use the following command:
sudo dnf remove eqp
eqp Package Contents on Fedora 36
/usr/bin/eqp
/usr/lib/.build-id
/usr/lib/.build-id/f1
/usr/lib/.build-id/f1/9172b135076f57607abd5f7f2540ee63d7654f
/usr/share/doc/eqp
/usr/share/doc/eqp/ChangeLog
/usr/share/doc/eqp/Manual.txt
/usr/share/doc/eqp/README
/usr/share/doc/eqp/basic.doc
/usr/share/doc/eqp/examples
/usr/share/doc/eqp/examples/33-basic
/usr/share/doc/eqp/examples/33-basic/DUAL-BA-5a.in
/usr/share/doc/eqp/examples/33-basic/DUAL-BA-5c.in
/usr/share/doc/eqp/examples/33-basic/LT-2.in
/usr/share/doc/eqp/examples/33-basic/LT-5.in
/usr/share/doc/eqp/examples/33-basic/LT-6.in
/usr/share/doc/eqp/examples/33-basic/LT-8.in
/usr/share/doc/eqp/examples/33-basic/QLT-1.in
/usr/share/doc/eqp/examples/33-basic/QLT-2.in
/usr/share/doc/eqp/examples/33-basic/QLT-3.in
/usr/share/doc/eqp/examples/33-basic/QLT-4.in
/usr/share/doc/eqp/examples/33-basic/QLT-5.in
/usr/share/doc/eqp/examples/33-basic/QLT-6.in
/usr/share/doc/eqp/examples/33-basic/RBA-2.in
/usr/share/doc/eqp/examples/README
/usr/share/doc/eqp/examples/ortholattice
/usr/share/doc/eqp/examples/ortholattice/e2.in
/usr/share/doc/eqp/examples/ortholattice/e3.in
/usr/share/doc/eqp/examples/ring
/usr/share/doc/eqp/examples/ring/x2.in
/usr/share/doc/eqp/examples/ring/x3.in
/usr/share/doc/eqp/examples/robbins
/usr/share/doc/eqp/examples/robbins/eqp-lemma0.in
/usr/share/doc/eqp/examples/robbins/eqp-lemma1.in
/usr/share/doc/eqp/examples/robbins/eqp-lemma2.in
/usr/share/doc/eqp/examples/robbins/eqp-lemma3.in
/usr/share/licenses/eqp
/usr/share/licenses/eqp/LICENSE
References
Summary
In this tutorial we learn how to install eqp on Fedora 36 using yum and [dnf]((/fedora/36/dnf/).