Q: Tranformation Programs FOL -> Normalform

Johann Schumann (schumann@informatik.tu-muenchen.de)
Fri, 7 Jan 1994 11:16:49 +0100

I am looking for implemented systems which transform
a formula in first order predicate logic into
Clausal normal form (and/or DNF, CNF, Negation Normal Form,
Definitional Normal Form),
and which perform Skolemization (optimised if possible).

A summary of the responses will be sent over the net

Thanks in advance
Johann Schumann
Intellektik - AI Research Group at the Chair of Computer Architecture
Institut fuer Informatik
Technische Universitaet Muenchen
80290 Muenchen, Germany
email: schumann@informatik.tu-muenchen.de