{"action":"created","issue":{"url":"https://api.github.com/repos/gapt/gapt/issues/389","labels_url":"https://api.github.com/repos/gapt/gapt/issues/389/labels{/name}","comments_url":"https://api.github.com/repos/gapt/gapt/issues/389/comments","events_url":"https://api.github.com/repos/gapt/gapt/issues/389/events","html_url":"https://github.com/gapt/gapt/issues/389","id":108598993,"number":389,"title":"Refactor expansion trees","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":[{"url":"https://api.github.com/repos/gapt/gapt/labels/Enhancement","name":"Enhancement","color":"0052cc"}],"state":"open","locked":false,"assignee":null,"milestone":null,"comments":3,"created_at":"2015-09-28T06:55:23Z","updated_at":"2015-11-26T15:16:38Z","closed_at":null,"body":"There should only be a single type for expansion trees.\r\n\r\nI'm not yet completely sure about the quantifier nodes:\r\n* Should we separate single/multiple quantifier nodes?  (I tend towards only having multiple quantifier nodes, which subsume single quantifier nodes.)\r\n* Should the number of instantiated quantifiers be the same for all children?  (I'd say yes.)"},"comment":{"url":"https://api.github.com/repos/gapt/gapt/issues/comments/159936180","html_url":"https://github.com/gapt/gapt/issues/389#issuecomment-159936180","issue_url":"https://api.github.com/repos/gapt/gapt/issues/389","id":159936180,"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-11-26T15:16:38Z","updated_at":"2015-11-26T15:16:38Z","body":"We discussed this yesterday in the gapt meeting, and reached the following conclusions:\r\n* There should be one single type for expansion trees, including merges.  Merges are necessary in the API to support merging of sub-trees, see for example #448 why this is important.\r\n* There should only be single quantifier nodes.  Multiple quantifier nodes are only needed for visualization in prooftool, for this application we should provide a matcher that converts the single quantifier nodes on-the-fly.  This matcher might also be necessary for the minimization algorithm, Sebastian wasn't sure about that."}}