# Source: eprover
# Package: eprover-examples
# Versions: eprover-examples (1.0.004-1)
# Prioritize: 43
Description: Theorem prover for first-order logic with equality - examples
 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.
 .
 This package contains several sample inputs to try E on.
Description-de: <trans>
 E ist ein vollautomatischer Theorembeweiser für vollständige
 Prädikatenlogik erster Stufe mit Gleichheit. Er akzeptiert eine
 mathematische
 Spezifikation und eine optionale Hypothese und versucht, die Hypothese zu
 beweisen und/oder eine Lösung zu finden, die ein (Gegen-)Modell für die
 Spezifikation darstellt.
 .
 E beruht auf einer Problemdarstellung nur durch Gleichungen und
 implementiert eine Variante des Superpositionskalküls. Die Beweissuche kann
 mit einer Vielzahl von Optionen oder einem leistungsfähigen automatischen
 Konfigurationsmodus geführt werden. Das System kann Eingaben in einer Reihe
 von verschiedenen Formaten, einschließlich der Standardformate TPTP-2 und
 TPTP-3. Er kann Beweisobjekte in den Formaten PCL2 oder TPTP-3/TSTP
 erzeugen.
 .
 E gilt als einer der mächtigsten und freundlichsten automatisierten
 Theorembeweiser für Prädikatenlogik. Er war immer wieder unter den besten
 Systemen in den wichtigsten Kategorien des CASC-Systemwettbewerbs und in
 der Regel das stärkste freie Softwaresystem.
 .
 <trans>

# other Descriptions of the eprover-examples package with a translation in de:
#