Note: If you decide not to go ahead with translating a description, please hit 'Abandon' below so others can have a go

Translating eprover

# Source: eprover
# Package(s): eprover
# Prioritize: 43
# Versions: eprover (1.0.004-1)

Short description

Untranslated: Theorem prover for first-order logic with equality
Translated (cs):

Long description

(Note: You must preserve the number of paragraphs)

Untranslated:

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.

Translated (cs): Non-breakspace note Textwrapping note
<trans> . <trans> . <trans>

Raw form:

# Source: eprover
# Package(s): eprover
# Prioritize: 43
# Versions: eprover (1.0.004-1)
# This Description is active
# This Description is owned
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-cs: <trans>
 <trans>
 .
 <trans>
 .
 <trans>
#
# other Descriptions of the eprover package with a translation in cs:
#