{"action":"created","issue":{"url":"https://api.github.com/repos/gapt/gapt/issues/373","labels_url":"https://api.github.com/repos/gapt/gapt/issues/373/labels{/name}","comments_url":"https://api.github.com/repos/gapt/gapt/issues/373/comments","events_url":"https://api.github.com/repos/gapt/gapt/issues/373/events","html_url":"https://github.com/gapt/gapt/pull/373","id":102735499,"number":373,"title":"Remove weakening in PCNF?","user":{"login":"gebner","id":313929,"avatar_url":"https://avatars.githubusercontent.com/u/313929?v=3","gravatar_id":"","url":"https://api.github.com/users/gebner","html_url":"https://github.com/gebner","followers_url":"https://api.github.com/users/gebner/followers","following_url":"https://api.github.com/users/gebner/following{/other_user}","gists_url":"https://api.github.com/users/gebner/gists{/gist_id}","starred_url":"https://api.github.com/users/gebner/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/gebner/subscriptions","organizations_url":"https://api.github.com/users/gebner/orgs","repos_url":"https://api.github.com/users/gebner/repos","events_url":"https://api.github.com/users/gebner/events{/privacy}","received_events_url":"https://api.github.com/users/gebner/received_events","type":"User","site_admin":false},"labels":[],"state":"closed","locked":false,"assignee":null,"milestone":null,"comments":2,"created_at":"2015-08-24T08:22:49Z","updated_at":"2015-09-01T15:33:45Z","closed_at":"2015-08-28T07:37:34Z","pull_request":{"url":"https://api.github.com/repos/gapt/gapt/pulls/373","html_url":"https://github.com/gapt/gapt/pull/373","diff_url":"https://github.com/gapt/gapt/pull/373.diff","patch_url":"https://github.com/gapt/gapt/pull/373.patch"},"body":"When we convert resolution proofs to LK, the proofs often begin with an axiom, weaken it with an extra copy of the formula, and then contract the copy away.  This seems to be caused by a call to `WeakeningMacroRule` in the PCNF code.\r\n\r\nI'm not entirely sure what the weakening is supposed to do, does anybody have any ideas?\r\n\r\nRemoving the weakenings does not cause any tests to fail."},"comment":{"url":"https://api.github.com/repos/gapt/gapt/issues/comments/136762849","html_url":"https://github.com/gapt/gapt/pull/373#issuecomment-136762849","issue_url":"https://api.github.com/repos/gapt/gapt/issues/373","id":136762849,"user":{"login":"gebner","id":313929,"avatar_url":"https://avatars.githubusercontent.com/u/313929?v=3","gravatar_id":"","url":"https://api.github.com/users/gebner","html_url":"https://github.com/gebner","followers_url":"https://api.github.com/users/gebner/followers","following_url":"https://api.github.com/users/gebner/following{/other_user}","gists_url":"https://api.github.com/users/gebner/gists{/gist_id}","starred_url":"https://api.github.com/users/gebner/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/gebner/subscriptions","organizations_url":"https://api.github.com/users/gebner/orgs","repos_url":"https://api.github.com/users/gebner/repos","events_url":"https://api.github.com/users/gebner/events{/privacy}","received_events_url":"https://api.github.com/users/gebner/received_events","type":"User","site_admin":false},"created_at":"2015-09-01T15:33:45Z","updated_at":"2015-09-01T15:33:45Z","body":"The regression tests didn't uncover any problems with this change."}}