Return-Path: Delivery-Date: Received: from antares.mcs.anl.gov (actually antares9.mcs.anl.gov !OR! qed-owner@mcs.anl.gov) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Fri, 7 Jan 1994 10:38:51 +0000 Received: by antares.mcs.anl.gov id AA01082 (5.65c/IDA-1.4.4 for qed-outgoing); Fri, 7 Jan 1994 04:18:01 -0600 Received: from tuminfo2.informatik.tu-muenchen.de by antares.mcs.anl.gov with SMTP id AA01052 (5.65c/IDA-1.4.4 for ); Fri, 7 Jan 1994 04:16:56 -0600 Received: from sunjessen16.informatik.tu-muenchen.de ([131.159.20.43]) by tuminfo2.informatik.tu-muenchen.de with SMTP id <57888>; Fri, 7 Jan 1994 11:16:29 +0100 Received: by sunjessen16.informatik.tu-muenchen.de id <8467>; Fri, 7 Jan 1994 11:16:56 +0100 From: Johann Schumann To: qed@mcs.anl.gov Subject: Q: Tranformation Programs FOL -> Normalform Cc: schumann@sunjessen16.informatik.tu-muenchen.de Message-Id: <94Jan7.111656met.8467@sunjessen16.informatik.tu-muenchen.de> Date: Fri, 7 Jan 1994 11:16:49 +0100 Sender: qed-owner@mcs.anl.gov 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 ------------------------------------------------------------ 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 ------------------------------------------------------------