{"action":"created","issue":{"url":"https://api.github.com/repos/gapt/gapt/issues/171","labels_url":"https://api.github.com/repos/gapt/gapt/issues/171/labels{/name}","comments_url":"https://api.github.com/repos/gapt/gapt/issues/171/comments","events_url":"https://api.github.com/repos/gapt/gapt/issues/171/events","html_url":"https://github.com/gapt/gapt/issues/171","id":55597974,"number":171,"title":"Improve Apply Methods of the Inference Rules","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/gapt/gapt/labels/Enhancement","name":"Enhancement","color":"0052cc"},{"url":"https://api.github.com/repos/gapt/gapt/labels/High%20Priority","name":"High Priority","color":"fbca04"},{"url":"https://api.github.com/repos/gapt/gapt/labels/Imported","name":"Imported","color":"FFFFFF"}],"state":"open","locked":false,"assignee":null,"milestone":null,"comments":6,"created_at":"2015-01-27T10:06:33Z","updated_at":"2015-02-02T10:05:37Z","closed_at":null,"body":"_From [bruno...@gmail.com](https://code.google.com/u/105016684496602932564/) on September 06, 2011 12:41:31_\n\nI have noticed the following lack of uniformity in the implementation of \"apply\" methods in inference rules:\r\n\r\n1) \"apply\" methods of propositional rules take only the auxiliary formulas and construct/compute the main formula.\r\n\r\n2) \"apply\" methods of quantifier rules, on the other hand, expect the main formula to be given as another argument. (Why is this so? In principle, the main formula could also be recomputed from the auxiliary formula together with an indication of which terms in the auxiliary formula should be replaced by a quantified variable.). They also check that the given main formula and the given auxiliary formula are \"compatible\", by calling an \"assert\" that checks whether instantiating the main formula gives a formula that is syntactically equal to the auxiliary formula.\r\n\r\n3) \"apply\" methods for equational rules are similar to those of quantifier rules, in the sense that it is necessary to pass the main formula as an argument. However, they don't check their own correctness as the quantifiers rule do with an \"assert\". (This is even a bit strange. As Giselle noticed today, the implementations of EqualityLeft1 and EqualityLeft2 are exactly the same, since in theory they only differ in the direction in which the equality is used and  in practice the correctness of the direction is simply not checked. Indeed, they check nothing at all and the responsibility of computing a correct main formula is left completely to the programmer.)\r\n\r\n\r\nI think option 1 above is the most useful. At least, that is the kind of behaviour that I need (or that would be more convenient to me) when implementing \"eliminateDefinitionRules\". And I think this behaviour is needed whenever one is reconstructing a proof in a top down way and making changes that may affect the auxiliary formulas: in such cases, it is convenient to simply reapply the inference rule to the new auxiliary formula, and let the inference recompute the new main formula.\r\n\r\nWhat do you think?\r\n\r\nAs I said, I need this behaviour for \"eliminateDefinitionRules\" (and I think), and therefore I am thinking about overloading the \"apply\" method for quantifier rules (and later on, equality rules too)... However, since I believe this kind of issue is quite common, I imagine that something similar (i.e. recomputing the main formula after new premises have been computed) might have already been implemented somewhere else, perhaps as part of some other algorithm that also does proof transformations in a top-down way.  So, if you know where I can find this code, please let me know!\r\n\r\nThis is related to Issue 48 . \r\nIt blocks Issue 167 . \r\nAnd the implementation of an apply method for equality rules blocks Issue 133 .\n\n_Original issue: http://code.google.com/p/gapt/issues/detail?id=171_"},"comment":{"url":"https://api.github.com/repos/gapt/gapt/issues/comments/72431777","html_url":"https://github.com/gapt/gapt/issues/171#issuecomment-72431777","issue_url":"https://api.github.com/repos/gapt/gapt/issues/171","id":72431777,"user":{"login":"shetzl","id":10726013,"avatar_url":"https://avatars.githubusercontent.com/u/10726013?v=3","gravatar_id":"","url":"https://api.github.com/users/shetzl","html_url":"https://github.com/shetzl","followers_url":"https://api.github.com/users/shetzl/followers","following_url":"https://api.github.com/users/shetzl/following{/other_user}","gists_url":"https://api.github.com/users/shetzl/gists{/gist_id}","starred_url":"https://api.github.com/users/shetzl/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/shetzl/subscriptions","organizations_url":"https://api.github.com/users/shetzl/orgs","repos_url":"https://api.github.com/users/shetzl/repos","events_url":"https://api.github.com/users/shetzl/events{/privacy}","received_events_url":"https://api.github.com/users/shetzl/received_events","type":"User","site_admin":false},"created_at":"2015-02-02T10:05:37Z","updated_at":"2015-02-02T10:05:37Z","body":"adding CCs from google code: @frehn @gisellemnr "}}