src/HOL/Tools/ATP_Manager/scripts/spass

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/ATP_Manager/scripts/spass	Wed Jul 28 18:32:54 2010 +0200
@@ -0,0 +1,19 @@
+#!/usr/bin/env bash
+#
+# Wrapper for SPASS that also outputs the Flotter-generated CNF (needed for
+# Isar proof reconstruction)
+#
+# Author: Jasmin Blanchette, TU Muenchen
+
+options=${@:1:$(($#-1))}
+name=${@:$(($#)):1}
+
+$SPASS_HOME/tptp2dfg $name $name.fof.dfg
+$SPASS_HOME/SPASS -Flotter $name.fof.dfg \
+    | sed 's/description({$/description({*/' \
+    > $name.cnf.dfg
+rm -f $name.fof.dfg
+cat $name.cnf.dfg
+$SPASS_HOME/SPASS $options $name.cnf.dfg \
+    | sed 's/\(Formulae used in the proof :\).*/\1 N\/A/'
+rm -f $name.cnf.dfg