Balík: eprover (1.0.004-1ubuntu1) [universe]
Odkazy pre eprover
Stiahnuť zdrojový balík eprover:
Original Maintainers (usually from Debian):
- Debian Science Maintainers (Konferencia)
- Petr Pudlak
It should generally not be necessary for users to contact the original maintainer.
- Domovská stránka [www.eprover.org]
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.
Ostatné balíky súvisiace s balíkom eprover
- rec: eprover-doc-html
- Theorem prover for first-order logic with equality - HTML doc
- sug: eprover-examples
- Theorem prover for first-order logic with equality - examples