https://github.com/JUrban/MPTP2
Tip revision: d27d2099befdb4bc86d0e312fbf6742db4719fba authored by Josef Urban on 22 February 2017, 13:23:11 UTC
simple looper for finding contradictions
simple looper for finding contradictions
Tip revision: d27d209
extract_e_refs.pl
#!/usr/bin/perl -w
# SYNOPSIS:
# Run E on provable problems and save proof premises into *.proof:
# for i in `cat 00proved`;do echo $i;
# eprover -l4 --pcl-compact --tstp-in -xAuto -tAuto $i | \
# epclextract --tstp-out | grep file > $i.proof; done
# Then extract the references into 00proofs:
# for i in `ls *.proof`; do extract_e_refs.pl $i; done > 00proofs
# extract the references from E proof in tstp syntax;
# put them into
# snow_proof( conjecture_name, th_or_def_names, bg_names)
use strict;
my @td_names = ();
my @bg_names = ();
my $conjecture = "";
while (<>)
{
(/^fof[^,]+,(axiom|conjecture).*\bfile\b[^,]+,([^\)]+)[\)].*/)
or die "Bad fof $_";
if ("conjecture" eq $1) { $conjecture = $2; }
else
{
my $ref = $2;
if ($ref =~ m/^ *[dt]\d+_/) { push(@td_names, $ref); }
else { push(@bg_names, $ref); }
}
}
die "No conjecture" if ($conjecture eq "");
print "snow_proof($conjecture, [";
print (join(",", @td_names), "],[", join(",", @bg_names));
print "]).\n";