{"action":"created","issue":{"url":"https://api.github.com/repos/newca12/gapt/issues/247","labels_url":"https://api.github.com/repos/newca12/gapt/issues/247/labels{/name}","comments_url":"https://api.github.com/repos/newca12/gapt/issues/247/comments","events_url":"https://api.github.com/repos/newca12/gapt/issues/247/events","html_url":"https://github.com/newca12/gapt/issues/247","id":55607600,"number":247,"title":"Some prover9 proof cannot be translated to LK.","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-Parsing","name":"Component-Parsing","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-Unspecified","name":"Milestone-Unspecified","color":"FFFFFF"},{"url":"https://api.github.com/repos/newca12/gapt/labels/Priority-High","name":"Priority-High","color":"FFFFFF"}],"state":"open","locked":false,"assignee":null,"milestone":null,"comments":4,"created_at":"2015-01-27T11:44:10Z","updated_at":"2015-01-27T11:44:28Z","closed_at":null,"body":"_From [fra...@gmail.com](https://code.google.com/u/108596877348066494139/) on November 11, 2013 22:55:29_\n\n* What steps will reproduce the problem?\r\n\r\ntptp.in:\r\nfof( to_prove, conjecture, ( ( ( ( ( ~'P'('0')) | ( ~( 'P'('s'('s'('a'))) => 'P'('s'('s'('s'('a')))) )) ) | ( ~( 'P'('a') => 'P'('s'('a')) )) ) | ( ( 'P'('s'('s'('s'('a')))) | ( ~'P'('s'('s'('a')))) ) & ( 'P'('s'('a')) | ( ~'P'('a')) ) ) ) | 'P'('s'('s'('s'('s'('0'))))) )).\r\n\r\ntptp_to_ladr \\< tptp.in > p9.in\r\nprover9 \\< p9.in > p9.out\r\n\r\nThen, in the gapt CLI:\r\n\r\nloadProver9LKProof( \"p9.out\" )\r\n\r\n\r\n* What is the expected output? What do you see instead?\r\n\r\nA proof imported from Prover9. Instead, the following exception is thrown:\r\n\r\njava.lang.IllegalArgumentException: clause:  :- ladr3(ladr1(ladr1(ladr0))), ladr3(ladr0) is not found in CNFs of ancestors: Set(ladr3(ladr1(ladr1(ladr1(ladr0)))) :- ) or Set( :- ladr3(ladr1(ladr1(ladr0))))\r\n        at at.logic.algorithms.resolution.PCNF$.PCNFn(PCNF.scala:114)\r\n        at at.logic.algorithms.resolution.PCNF$.PCNFn(PCNF.scala:109)\r\n        at at.logic.algorithms.resolution.PCNF$.apply(PCNF.scala:54)\r\n        at at.logic.algorithms.resolution.RobinsonToLK$$anonfun$apply$1.apply(robinson.scala:30)\r\n        at at.logic.algorithms.resolution.RobinsonToLK$$anonfun$apply$1.apply(robinson.scala:30)\r\n        at at.logic.algorithms.resolution.RobinsonToLK$.recConvert(robinson.scala:69)\r\n[...]\r\n\r\nMaybe weakening is missing? In my working copy, I'm using the following\r\nwhich adds weakenings to a proof to \"complete\" a sequent. I of course lifted that code from introduceContractions :-)\r\n\r\n  /**\r\n  * introduce weakenings to recover the end-sequent (if a formula is not used in\r\n  * the proof.)\r\n  */\r\n  def introduceWeakenings(resp: LKProof, s: FSequent): LKProof= {\r\n    println(\" *****************     introducing weakenings ****************** \")\r\n    // for each formula F in s, count its occurrences in s and resp and apply weakenings on resp until we reach the same number\r\n    val p1 = s.antecedent.toSet.foldLeft(resp)((p,f) =>\r\n      ((1).to(s.antecedent.filter(_ == f).size - p.root.antecedent.filter(_.formula == f).size)).foldLeft(p)((q,n) =>\r\n        WeakeningLeftRule(q,f) ))\r\n    val p2 = s.succedent.toSet.foldLeft(p1)((p,f) =>\r\n      ((1).to(s.succedent.filter(_ == f).size - p.root.succedent.filter(_.formula == f).size)).foldLeft(p)((q,n) =>\r\n        WeakeningRightRule(q,f) ))\r\n    println(\" *****************   new end-sequent: \" + p2.root + \" ****************** \")\r\n    p2\r\n  }\r\n\r\n\r\nCould someone in the know about the RobinsonToLK algorithm have a look at this? Thanks!\n\n_Original issue: http://code.google.com/p/gapt/issues/detail?id=247_"},"comment":{"url":"https://api.github.com/repos/newca12/gapt/issues/comments/71633798","html_url":"https://github.com/newca12/gapt/issues/247#issuecomment-71633798","issue_url":"https://api.github.com/repos/newca12/gapt/issues/247","id":71633798,"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:44:28Z","updated_at":"2015-01-27T11:44:28Z","body":"_From [Martin.R...@googlemail.com](https://code.google.com/u/113922991942493634983/) on November 12, 2013 07:43:29_\n\nThis issue was closed by revision r1733 .\n\n**Status:** Fixed  \n"}}