DDTP - Übersetzung für einen Theorembeweiser

[Martin Eberhard Schauer <Martin.E.Schauer@gmx.de>]

                               Hallo,

wir arbeiten an der Übersetzung für eprover (1). Zwei Sätze sind für den
Nicht-Mathematiker nicht trivial.

E is a fully automatic theorem prover for full first-order logic with
equality.

... and implements a variant of the superposition calculus.

Was sind gebräuchliche/verständliche Übersetzungen für first-order logic
und superposition calculus?

Ein gespanntes Danke im voraus,
   Martin

1: http://ddtp.debian.net/ddtss/index.cgi/de/forreview/eprover?1314548792