{"action":"created","issue":{"url":"https://api.github.com/repos/newca12/gapt/issues/258","labels_url":"https://api.github.com/repos/newca12/gapt/issues/258/labels{/name}","comments_url":"https://api.github.com/repos/newca12/gapt/issues/258/comments","events_url":"https://api.github.com/repos/newca12/gapt/issues/258/events","html_url":"https://github.com/newca12/gapt/issues/258","id":55608302,"number":258,"title":"LKtoLKsk fails on the n-tape proof","user":{"login":"newca12","id":543542,"avatar_url":"https://avatars.githubusercontent.com/u/543542?v=3","gravatar_id":"","url":"https://api.github.com/users/newca12","html_url":"https://github.com/newca12","followers_url":"https://api.github.com/users/newca12/followers","following_url":"https://api.github.com/users/newca12/following{/other_user}","gists_url":"https://api.github.com/users/newca12/gists{/gist_id}","starred_url":"https://api.github.com/users/newca12/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/newca12/subscriptions","organizations_url":"https://api.github.com/users/newca12/orgs","repos_url":"https://api.github.com/users/newca12/repos","events_url":"https://api.github.com/users/newca12/events{/privacy}","received_events_url":"https://api.github.com/users/newca12/received_events","type":"User","site_admin":false},"labels":[{"url":"https://api.github.com/repos/newca12/gapt/labels/1%20star","name":"1 star","color":"FFFFFF"},{"url":"https://api.github.com/repos/newca12/gapt/labels/bug","name":"bug","color":"FFFFFF"},{"url":"https://api.github.com/repos/newca12/gapt/labels/Component-ProofTransformations","name":"Component-ProofTransformations","color":"FFFFFF"},{"url":"https://api.github.com/repos/newca12/gapt/labels/imported","name":"imported","color":"FFFFFF"},{"url":"https://api.github.com/repos/newca12/gapt/labels/Milestone-Release7.0","name":"Milestone-Release7.0","color":"FFFFFF"},{"url":"https://api.github.com/repos/newca12/gapt/labels/Priority-Medium","name":"Priority-Medium","color":"FFFFFF"}],"state":"open","locked":false,"assignee":null,"milestone":null,"comments":2,"created_at":"2015-01-27T11:51:22Z","updated_at":"2015-01-27T11:51:29Z","closed_at":null,"body":"_From [Martin.R...@googlemail.com](https://code.google.com/u/113922991942493634983/) on December 09, 2013 14:21:14_\n\nThis error comes with a change in llk parsing (axiom instantiations are not done by cut anymore) and produces an error in LKtoLKsk which I don't fully understand. On the commandline you can reporoduce it by issuing the following commands:\r\n\r\n    val p = loadLLK(\"algorithms/hlk/src/test/resources/tape3.llk\")\r\n    val elp = eliminateDefinitions(p, \"TAPEPROOF\")\r\n    val selp = at.logic.transformations.skolemization.lksk.LKtoLKskc(regularize(elp)._1)\r\n\r\nand get:\r\nat.logic.calculi.lk.base.LKUnaryRuleCreationException: Could not create lk rule Auxiliary formula occurrence label of ForallSkLeftRule does not contain substitution term. Label: Set(), substitution term: 0:ι from parent List(∀y:ι.=(bm(+(0:ι, 1:ι):ι, +(y:ι, 1:ι):ι):ι, bm(0:ι, y:ι):ι): o (label: Set())) :- List(=(bm(+(0:ι, 1:ι):ι, +(0:ι, 1:ι):ι):ι, bm(0:ι, 0:ι):ι): o (label: Set())) with auxiliary formulas ∀y:ι.=(bm(+(0:ι, 1:ι):ι, +(y:ι, 1:ι):ι):ι, bm(0:ι, y:ι):ι): o\r\n\tat at.logic.calculi.lksk.ForallSkLeftRule$.apply(lksk.scala:110)\r\n\tat at.logic.algorithms.lksk.applySubstitution$.apply(substitution.scala:56)\r\n\tat at.logic.algorithms.lksk.applySubstitution$.apply(substitution.scala:82)\r\n\tat at.logic.algorithms.lksk.applySubstitution$.apply(substitution.scala:82)\r\n[...]\r\n\tat at.logic.transformations.skolemization.lksk.LKtoLKskc$.rec(lksk.scala:99)\r\n\tat at.logic.transformations.skolemization.lksk.LKtoLKskc$.rec(lksk.scala:89)\r\n\tat at.logic.transformations.skolemization.lksk.LKtoLKskc$.rec(lksk.scala:179)\r\n\tat at.logic.transformations.skolemization.lksk.LKtoLKskc$.rec(lksk.scala:286)\r\n\tat at.logic.transformations.skolemization.lksk.LKtoLKskc$.rec(lksk.scala:286)\r\n\tat at.logic.transformations.skolemization.lksk.LKtoLKskc$.transformWeakQuantRule(lksk.scala:390)\r\n\tat at.logic.transformations.skolemization.lksk.LKtoLKskc$.rec(lksk.scala:81)\r\n[...]\r\n\r\nWith the commands:\r\n\r\n    val selp = try { at.logic.transformations.skolemization.lksk.LKtoLKskc(regularize(elp)._1) } catch { case LKUnaryRuleCreationException(_,p,aux::Nil) => println(aux); p }\r\n    prooftool(selp)\r\n\r\nyou can see the subproof with the wrong label, the logger should print the end-sequent of the parent in the rec(...) call, but i can't really match the labels.\r\n\r\nMight this be failing because the selection of aux formulas is done by formula which might have the wrong label if there is more than one occurrence of aux in a sequent?\n\n_Original issue: http://code.google.com/p/gapt/issues/detail?id=258_"},"comment":{"url":"https://api.github.com/repos/newca12/gapt/issues/comments/71634858","html_url":"https://github.com/newca12/gapt/issues/258#issuecomment-71634858","issue_url":"https://api.github.com/repos/newca12/gapt/issues/258","id":71634858,"user":{"login":"newca12","id":543542,"avatar_url":"https://avatars.githubusercontent.com/u/543542?v=3","gravatar_id":"","url":"https://api.github.com/users/newca12","html_url":"https://github.com/newca12","followers_url":"https://api.github.com/users/newca12/followers","following_url":"https://api.github.com/users/newca12/following{/other_user}","gists_url":"https://api.github.com/users/newca12/gists{/gist_id}","starred_url":"https://api.github.com/users/newca12/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/newca12/subscriptions","organizations_url":"https://api.github.com/users/newca12/orgs","repos_url":"https://api.github.com/users/newca12/repos","events_url":"https://api.github.com/users/newca12/events{/privacy}","received_events_url":"https://api.github.com/users/newca12/received_events","type":"User","site_admin":false},"created_at":"2015-01-27T11:51:29Z","updated_at":"2015-01-27T11:51:29Z","body":"_From [fra...@gmail.com](https://code.google.com/u/108596877348066494139/) on December 09, 2013 08:25:24_\n\nFixed in r1822 .\n\n**Status:** Fixed  \n"}}