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
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.
Jannik Vierling
@jvierling
@andreasfrom Have you tried to import the problems with 'TipSmtImporter.fixupAndLoad'. This uses the external tip-tools in order to do some preprocessing (monomorphisation, replacing int by nat, etc) on the problems.
Andreas H. From
@andreasfrom
@jannikvierling Yes, sorry I should have said I did try that, but it didn't seem to make much of a difference, giving me errors directly from the tip tool instead. Here is an example where fixupAndLoad just gives a different error (because of this, I think):
scala> val problem = TipSmtImporter.fixupAndLoad("benchmarks/isaplanner/prop_02.smt2")
java.util.NoSuchElementException: None.get
Jannik Vierling
@jvierling
Our Tip importer not very sophisticated so for the moment we will have to deal with certain cases where the error messages are not very comprehensible. However when using 'fixupAndLoad' many more problems can be parsed.
Andreas H. From
@andreasfrom
Okay, I will use that one instead. Thanks!
Jannik Vierling
@jvierling
If you need the importer to support any features that it can't currently handle, then let me know so that I can implement them.
Andreas H. From
@andreasfrom
Adding axioms one at a time and doing a couple of loops in between improves spind a bit. I think testing axioms before adding them might potentially help a lot. (timeout also increased from 30s to 45s)
mode
analytic_independent    17
analytic_sequential     40
spind                   15
treegrammar              7
Stefan Hetzl
@shetzl
@andreasfrom This looks better!
I could very well image that testing is quite useful.
It may also be worthwhile to have a closer look at the difference between independent and sequential induction axioms, maybe spind can somehow emulate the use of the sequential induction axioms
Jannik Vierling
@jvierling
@andreasfrom I have updated the tip tool on the server. The problems should now parse.
Andreas H. From
@andreasfrom
@shetzl Yes, I will look at what @jannikvierling sent me and take a closer look.
@jannikvierling Great, thank you!
Gabriel Ebner
@gebner
@andreasfrom Are you planning on doing any experiments on clogic89 between now and Thursday?
Gabriel Ebner
@gebner
@andreasfrom I'm running some experiments on clogic89 today. Please don't run anything else at the moment.
Gabriel Ebner
@gebner
@andreasfrom Also using clogic89 today.
Ermine516
@Ermine516
@jannikvierling Sorry I was delayed in message you, Vacation :)
I am back now
Is there a gapt meeting today?
Gabriel Ebner
@gebner
No, happy easter!
Ermine516
@Ermine516
If so I can bring it with me and we can discuss
:D, ah yes that is why I was on vacation, right.
Happy easter to you too
see you next week then
Gabriel Ebner
@gebner
Next week is labor day.
Ermine516
@Ermine516
ok, I should look at my calendar then
Andreas H. From
@andreasfrom
@gebner Sorry, didn't see your message. I only ran some stuff yesterday. If you need it today and tomorrow please let me know.
Gabriel Ebner
@gebner
Nah, everything's already done now. Also the deadline got extended by two weeks, so I'm no longer in such a hurry either.