Summary: Automated theorem prover for first-order equational logic
Name: eqp
Version: 09e
Release: 3%{?dist}
License: Freely redistributable without restriction
URL: http://www.cs.unm.edu/~mccune/eqp/
Group: Applications/Engineering
Source0: http://www.cs.unm.edu/~mccune/old-ftp/eqp-09e.tar.gz
# file to clarify the software license
Patch0: eqp-09e-license.patch
# patches for some missing function prototypes
Patch1: eqp-09e-missing-proto.patch
# patches for printing of pointer variables
Patch2: eqp-09e-printf.patch
%description
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 formal proof, or a counter-example of
this conjecture. 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 %{_docdir}/%{name}-%{version}/examples/robbins/
%prep
%setup -q
%patch0 -p1 -b .license
%patch1 -p1 -b .missing-proto
%patch2 -p1 -b .printf
%build
# upstream does not use autoconf, just run make
make CFLAGS="${RPM_OPT_FLAGS} -DTP_RUSAGE" eqp
%install
# install the executable as "eqp"
install -d ${RPM_BUILD_ROOT}%{_bindir}
install -m 755 eqp%{version} ${RPM_BUILD_ROOT}%{_bindir}/eqp
# remove the execute permissions from the "go" script in the examples
chmod 644 examples/go
%files
%doc ChangeLog Manual.txt LICENSE README basic.doc examples
%attr(0755,root,root) %{_bindir}/eqp
%changelog
* Thu Nov 01 2012 John C. Peterson - 09e-3
- Removed the defattr line (as it is now obsolete)
* Fri Dec 23 2011 John C. Peterson - 09e-2
- Changed license terms to "Freely redistributable without restriction"
- Eliminated the makefile patch and adjusted the make command accordingly
- Eliminated the lont-int patch and crafted a new one (eqp-09e-printf.patch)
that uses the pointer conversion flag in the relevant printf statements
- Removed all execute permission bits from the examples/go script
- Some minor, cosmetic changes to the spec file
* Sat Dec 17 2011 John C. Peterson - 09e-1
- Initial package spec file for Fedora / Red Hat Enterprise Linux
- Patches for some missing function prototypes
- Patches for long int on 64 bit architectures