{"action":"closed","issue":{"url":"https://api.github.com/repos/gapt/gapt/issues/79","labels_url":"https://api.github.com/repos/gapt/gapt/issues/79/labels{/name}","comments_url":"https://api.github.com/repos/gapt/gapt/issues/79/comments","events_url":"https://api.github.com/repos/gapt/gapt/issues/79/events","html_url":"https://github.com/gapt/gapt/issues/79","id":55583266,"number":79,"title":"Set of Support Refinement","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/Imported","name":"Imported","color":"FFFFFF"},{"url":"https://api.github.com/repos/gapt/gapt/labels/Low%20priority","name":"Low priority","color":"006b75"}],"state":"closed","locked":false,"assignee":null,"milestone":null,"comments":7,"created_at":"2015-01-27T07:04:03Z","updated_at":"2015-11-05T08:08:52Z","closed_at":"2015-11-05T08:08:52Z","body":"_From [shaoli...@gmail.com](https://code.google.com/u/113190107447576027220/) on August 07, 2010 11:50:31_\n\nThe set of support refinement should be added to ATP:\r\n1) The extension to the Refinement interface should be created, maybe by having all clauses in the set of support appearing at the beginning of the queue and therefore not being used among themselves to resolve.\r\n2) We need to be able to decide the set of support at the beginning. Maybe in the clause insertion syntax we also need to specify if the clause is an axiom of the theory so we can later use this information automatically to include this clause in the set of support.\r\n\r\nBruno, you expressed some wish to have this feature. Do you have any thing to say about this issue? Do you want to implement this?\n\n_Original issue: http://code.google.com/p/gapt/issues/detail?id=79_"}}