How To Install eqp on Fedora 36

In this tutorial we learn how to install eqp in Fedora 36. eqp is Automated theorem prover for first-order equational logic

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/).