by

Where communities thrive


  • Join over 1.5M+ people
  • Join over 100K+ communities
  • Free without limits
  • Create your own community
People
Repo info
Activity
Ermine516
@Ermine516
It works
Ermine516
@Ermine516
@gebner there seems to be a problem with the import. That file is 6k long yet the proof constructed in gapt is 15 sequents long and one axiom.
Gabriel Ebner
@gebner
It looks like there is a much shorter proof. :-) Some data: in order to parse the proof, we convert it using prooftrans ivy. This blows the proof up to 22k inferences. The massive reduction then happens in fixDerivation, where we add extra inferences to make sure that the input clauses match up with our clausification. Not sure why the proof gets smaller here.
Gabriel Ebner
@gebner
Ok, found the bug. This was interesting. So as explained above, we parse the proof from the ivy format produced by prooftrans ivy. However we parse the input formulas of the original problem directly from the prover9 file. Interestingly, backslashes are escaped in the ivy format---they are written as backslash_for_ivy. The translation code was originally written by Martin many years ago and mapped the ivy backslash to a double backslash.
Now fixDerivation found an input clause with two backslashes and couldn't find it in the end-sequent. So it called Escargot: please derive the clause with the double backslash. And Escargot returned a (very short) proof of the empty clause...
Ermine516
@Ermine516
So it is still not working I guess
I think I should get rid of the backslashes
Gabriel Ebner
@gebner
No, it works now. At least I get a proof with ~20k inferences.
Ermine516
@Ermine516
Perfect thanks
Andreas H. From
@andreasfrom
I just realized I didn't get an email, so I guess there's no meeting today?
Stefan Hetzl
@shetzl
@andreasfrom: Sorry, I forgot to send the announcement per email. There is in fact a meeting today at 14:30.
Andreas H. From
@andreasfrom
Glad to hear, then I didn't stay on campus for nothing :-)
Ermine516
@Ermine516
Question I got this message
java.lang.OutOfMemoryError: Java heap space
  at scala.collection.immutable.HashSet$HashTrieSet.updated0(HashSet.scala:554)
  at scala.collection.immutable.HashSet.$plus(HashSet.scala:84)
  at scala.collection.immutable.HashSet.$plus(HashSet.scala:35)
  at scala.collection.mutable.SetBuilder.$plus$eq(SetBuilder.scala:28)
  at scala.collection.mutable.SetBuilder.$plus$eq(SetBuilder.scala:24)
  at scala.collection.TraversableLike.$anonfun$map$1(TraversableLike.scala:237)
  at scala.collection.TraversableLike$$Lambda$74/1911152052.apply(Unknown Source)
How do I increase the heap space when running gapt?
Gabriel Ebner
@gebner
How do you run gapt?
Ermine516
@Ermine516
./gapt.sh
Gabriel Ebner
@gebner
$ ./gapt.sh -h                                             Wed 10 Apr 2019 03:34:35 PM CEST
GAPT Command Line Interface

usage: gapt.sh [-h] [-m MEM]

   -m : give MEM amount of memory to the java virtual machine (default: 2g)
Ermine516
@Ermine516
Thanks
Ermine516
@Ermine516
BTW, @gebner how long did it take to get the 20K inference proof.
I have been running the following
Prover9Importer.expansionProof("Mich.pf")
for a little less than an hour
Gabriel Ebner
@gebner
Well, extracting expansion proofs from resolution proofs has an exponential lower bound on the worst case runtime. I didn't try to extract an expansion proof from the one you sent me yet.
Ermine516
@Ermine516
ok what I thought was wrong
Ermine516
@Ermine516
Hello all, I think I found a weird bug in cut-introduction.
So there are proof where a pi_1 cut seems not to exist
I mean pi_1 with 1 quantifier prefix
so I try to introduce a pi_1 cut with a 2 quantifier prefix
which works
but one of the quantifiers does not do anything, i.e. it does not appear in the formula
any idea why
here is the JSON
{
  "0" : {"name" : "LogicalAxiom", "A" : "v0 / K(v2, v1) * K(v2, v1) = v0"},
  "1" : {
    "name" : "ForallLeftRule",
    "subProof" : 0,
    "aux" : -1,
    "A" : "v0 / v1_0 * v1_0 = v0",
    "term" : "K(v2, v1)",
    "v" : "v1_0"
  },
  "2" : {
    "name" : "ForallLeftRule",
    "subProof" : 1,
    "aux" : -1,
    "A" : "∀v1_0 v0_0 / v1_0 * v1_0 = v0_0",
    "term" : "v0",
    "v" : "v0_0"
  },
  "3" : {"name" : "LogicalAxiom", "A" : "K(v2, v1) * 1 = K(v2, v1)"},
  "4" : {
    "name" : "ForallLeftRule",
    "subProof" : 3,
    "aux" : -1,
    "A" : "v0_0 * 1 = v0_0",
    "term" : "K(v2, v1)",
    "v" : "v0_0"
  },
  "5" : {
    "name" : "LogicalAxiom",
    "A" : "1 * (v0 / K(v2, v1) * K(v2, v1)) = v0 / K(v2, v1) * K(v2, v1)"
  },
  "6" : {
    "name" : "ForallLeftRule",
    "subProof" : 5,
    "aux" : -1,
    "A" : "1 * v0_0 = v0_0",
    "term" : "v0 / K(v2, v1) * K(v2, v1)",
    "v" : "v0_0"
  },
  "7" : {
    "name" : "LogicalAxiom",
    "A" : "v0 / K(v2, v1) * K(v2, v1) * (1 * (v0 / K(v2, v1) * K(v2, v1))) =\n  v0 / K(v2, v1) * (K(v2, v1) * 1) * (v0 / K(v2, v1)) * K(v2, v1)"
  },
  "8" : {
    "name" : "ForallLeftRule",
    "subProof" : 7,
    "aux" : -1,
    "A" : "v0 / K(v2, v1) * K(v2, v1) * (v2_0 * (v0 / K(v2, v1) * K(v2, v1))) =\n  v0 / K(v2, v1) * (K(v2, v1) * v2_0) * (v0 / K(v2, v1)) * K(v2, v1)",
    "term" : "1",
    "v" : "v2_0"
  },
  "9" : {
    "name" : "ForallLeftRule",
    "subProof" : 8,
    "aux" : -1,
    "A" : "∀v2_0\n  v0 / K(v2, v1) * v1_0 * (v2_0 * (v0 / K(v2, v1) * v1_0)) =\n    v0 / K(v2, v1) * (v1_0 * v2_0) * (v0 / K(v2, v1)) * v1_0",
    "term" : "K(v2, v1)",
    "v" : "v1_0"
  },
  "10" : {
    "name" : "ForallLeftRule",
    "subProof" : 9,
    "aux" : -1,
    "A" : "∀v1_0\n  ∀v2_0\n  v0_0 * v1_0 * (v2_0 * (v0_0 * v1_0)) = v0_0 * (v1_0 * v2_0) * v0_0 * v1_0",
    "term" : "v0 / K(v2, v1)",
    "v" : "v0_0"
  },
  "11" : {
    "name" : "ReflexivityAxiom",
    "s" : "v0 / K(v2, v1) * K(v2, v1) * (1 * (v0 / K(v2, v1) * K(v2, v1)))"
  },
  "12" : {
    "name" : "WeakeningLeftRule",
    "subProof" : 11,
    "formula" : "v0 / K(v2, v1) * K(v2, v1) * (1 * (v0 / K(v2, v1) * K(v2, v1))) =\n  v0 / K(v2, v1) * (K(v2, v1) * 1) * (v0 / K(v2, v1)) * K(v2, v1)"
  },
  "13" : {
    "name" : "EqualityRightRule",
    "subProof" : 12,
    "eq" : -1,
    "aux" : 0,
    "replacementContext" : "λx x = v0 / K(v2, v1) * K(v2, v1) * (1 * (v0 / K(v2, v1) * K(v2, v1)))"
  },
  "14" : {
    "name" : "CutRule",
    "leftSubProof" : 10,
    "aux1" : 0,
    "rightSubProof" : 13,
    "aux2" : -1
  },
  "15" : {
    "name" : "WeakeningLeftRule",
    "subProof" : 14,
    "formula" : "1 * (v0 / K(v2, v1) * K(v2, v1)) = v0 / K(v2, v1) * K(v2, v1)"
  },
  "16" : {
    "name" : "EqualityRightRule",
    "subProof" : 15,
    "eq" : -1,
    "aux" : 0,
    "replacementContext" : "λx\n  v0 / K(v2, v1) * (K(v2, v1) * 1) * (v0 / K(v2, v1)) * K(v2, v1) =\n    v0 / K(v2, v1) * K(v2, v1) * x"
  },
  "17" : {
    "name" : "CutRule",
    "leftSubProof" : 6,
    "aux1" : 0,
    "rightSubProof" : 16,
    "aux2" : -1
  },
  "18" : {
    "name" : "WeakeningLeftRule",
    "subProof" : 17,
    "formula" : "K(v2, v1) * 1 = K(v2, v1)"
  },
  "19" : {
    "name" : "EqualityRightRule",
    "subProof" : 18,
    "eq" : -1,
    "aux" : 0,
    "replacementContext" : "λx\n  v0 / K(v2, v1) * x * (v0 / K(v2, v1)) * K(v2, v1) =\n    v0 / K(v2, v1) * K(v2, v1) * (v0 / K(v2, v1) * K(v2, v1))"
  },
  "20" : {
    "name" : "CutRule",
    "leftSubProof" : 4,
    "aux1" : 0,
    "rightSubProof" : 19,
    "aux2" : -1
  },
  "21" : {
    "name" : "LogicalAxiom",
    "A" : "'\\\\'(v0 / K(v2, v1) * K(v2, v1) * (v0 / K(v2, v1)),\n      v0 / K(v2, v1) * K(v2, v1) * (v0 / K(v2, v1) * K(v2, v1))) =\n  L(K(v2, v1), v0 / K(v2, v1), v0 / K(v2, v1) * K(v2, v1))"
  },
  "22" : {
    "name" : "ForallLeftRule",
    "subProof" : 21,
    "aux" : -1,
    "A" : "'\\\\'(v0 / K(v2, v1) * K(v2, v1) * (v0 / K(v2, v1)),\n      v0 / K(v2, v1) * K(v2, v1) * (v0 / K(v2, v1) * v2_0)) =\n  L(v2_0, v0 / K(v2, v1), v0 / K(v2, v1) * K(v2, v1))",
    "term" : "K(v2, v1)",
    "v" : "v2
Seems like there is a limit :/
I'll send by e-mail to those who need
Ermine516
@Ermine516
also got a stackoverflow when trying to introduce 4 quantifiers
Andreas H. From
@andreasfrom
So I'm looking at these TIP problems and most of them just don't parse. Is this expected?
status
failed                       54
ok                           68
parsing_other_exception    1784
viper_timeout               266
Each file appears 4 times in those numbers.
Out of the 'ok' ones this is the mode breakdown:
mode
analytic_independent    17
analytic_sequential     39
spind                    6
treegrammar              6
Jannik Vierling
@jvierling
@Ermine516 Please send me the file by email
Jannik Vierling
@jvierling
@andreasfrom I will look into that
Andreas H. From
@andreasfrom
@jannikvierling nice, thank you. Most of them are malformed datatypes declaration exceptions and some are malformed expression. I'm running on the problems from the testing/TIP/tip-benchmarks-9c0088b73457ffbdb79159d487c9db2deb650381.tar.gz file in the repository.
Stefan Hetzl
@shetzl
@andreasfrom : Thanks for running the tests!
It is surprising to me that spind is significantly worse that analytic_sequential and analytic_indepedent.
It should be possible to be as good as / better than these without having to invest too much effort.
@jannikvierling Do you have some documentation about the analytic induction axioms that you could send Andreas?
@andreasfrom what does return status "failed" mean? I assume that "ok" means a proof has been found.
Jannik Vierling
@jvierling
@andreasfrom I will send you some notes I took about the independent and sequential induction axioms.
Andreas H. From
@andreasfrom
@jannikvierling Failed means saturated without finding a proof. So I guess it maybe doesn't always make sense to call it failed actually.