a b c d e f g h i j k l m n o p q r s t u v w x y z
Description: Theorem prover for first-order logic with equality
E is a fully automatic theorem prover for full first-order logic with
equality. It accepts a mathematical specification and, optionally, a
hypothesis, and tries to prove the hypothesis and/or find a
saturation representing a (counter-)model for the specification.
.
E is based on a purely equational problem representation and
implements a variant of the superposition calculus. Proof search can
be guided with a multitude of options or a powerful automatic
configuration mode. The system can process input in a number of
different formats, including the standard TPTP-2 and TPTP-3
formats. It can generate proof objects in PCL2 or TPTP-3/TSTP
format.
.
E is considered one of the most powerful and friendly automated
theorem provers for first-order logic. It has consistently been among
the top system in the major categories of the CASC system competition,
and usually been the strongest free software system.
Description: Equational theorem prover
This package provides tools to prove equational theorems:
from a mathematical specification in many-sorted first-order
logic with equality and an hypothesis/conjecture, it
will look for a proof.
--- 57519 Thu Jan 1 00:00:00 1970
+++ 292308 Thu Jan 1 00:00:00 1970
@@ -1,18 +1,5 @@
-Theorem prover for first-order logic with equality
+Equational theorem prover
- E is a fully automatic theorem prover for full first-order logic with
+ This package provides tools to prove equational theorems:
- equality. It accepts a mathematical specification and, optionally, a
+ from a mathematical specification in many-sorted first-order
- hypothesis, and tries to prove the hypothesis and/or find a
+ logic with equality and an hypothesis/conjecture, it
- saturation representing a (counter-)model for the specification.
+ will look for a proof.
- .
- E is based on a purely equational problem representation and
- implements a variant of the superposition calculus. Proof search can
- be guided with a multitude of options or a powerful automatic
- configuration mode. The system can process input in a number of
- different formats, including the standard TPTP-2 and TPTP-3
- formats. It can generate proof objects in PCL2 or TPTP-3/TSTP
- format.
- .
- E is considered one of the most powerful and friendly automated
- theorem provers for first-order logic. It has consistently been among
- the top system in the major categories of the CASC system competition,
- and usually been the strongest free software system.