src/HOL/Tools/ATP_Manager/SPASS_TPTP
author blanchet
Mon, 26 Jul 2010 11:19:57 +0200
changeset 37990 586130f71c78
parent 37962 d7dbe01f48d7
permissions -rwxr-xr-x
remove confusing line in SPASS output (because the axiom names are off -- bug in SPASS)

#!/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