Prover9: When proving a formula, we replace free variables by constants (which corresponds to proving the universal closure).

Thanks to Martin's recent fixes, we can now use prover9 in cut-introduction, e.g. (in the CLI):

:load ../examples/ProofSequences.scala

val p = LinearExampleProof(8)
val prover = new at.logic.provers.prover9.Prover9Prover()
cutIntroExp(p, prover)

Somehow though, the parsing of prover9 to a resolution refutation (RobinsonProof) seems rather slow, sometimes significantly slower than the built-in LK proof-search:

/*
p9.out was obtained by refuting the following tptp:
fof( to_prove, conjecture, ( ( ( ( ( ( 'P'('0') & ( 'P'('s'('s'('s'('s'('α'))))) => 'P'('s'('s'('s'('s'('s'('α')))))) ) ) & ( 'P'('α') => 'P'('s'('α')) ) ) & ( 'P'('s'('s'('s'('s'('s'('α')))))) => 'P'('s'('s'('s'('s'('s'('s'('α'))))))) ) ) & ( 'P'('s'('α')) => 'P'('s'('s'('α'))) ) ) & ( ( ( ( 'P'('s'('s'('α'))) | ( ~'P'('s'('α'))) ) & ( 'P'('s'('s'('s'('s'('s'('s'('α'))))))) | ( ~'P'('s'('s'('s'('s'('α')))))) ) ) & ( 'P'('s'('α')) | ( ~'P'('α')) ) ) => ( ( ( ( 'P'('s'('s'('s'('s'('0'))))) | ( ~'P'('s'('s'('s'('0'))))) ) & ( 'P'('s'('s'('s'('s'('s'('s'('s'('s'('0'))))))))) | ( ~'P'('s'('s'('s'('s'('s'('s'('0')))))))) ) ) & ( 'P'('s'('s'('s'('0')))) | ( ~'P'('s'('s'('0')))) ) ) & ( ( ( 'P'('s'('s'('0'))) | ( ~'P'('s'('0'))) ) & ( 'P'('s'('s'('s'('s'('s'('s'('0'))))))) | ( ~'P'('s'('s'('s'('s'('0')))))) ) ) & ( 'P'('s'('0')) | ( ~'P'('0')) ) ) ) ) ) => 'P'('s'('s'('s'('s'('s'('s'('s'('s'('0'))))))))) )).
*/

def test() = {
  var start = scala.compat.Platform.currentTime
  val p = loadProver9Proof( "/tmp/p9/p9.out" )
  println( "prover9: " + (scala.compat.Platform.currentTime - start))
  start = scala.compat.Platform.currentTime
  proveProp( p._2 )
  println( "proveProp: " + (scala.compat.Platform.currentTime - start))
}

test()
// result:
// prover9: 9371ms
// proveProp: 628ms



git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1737 85d21ef8-add0-11de-ae77-5bfb9c5a3f34