{"action":"created","issue":{"url":"https://api.github.com/repos/newca12/gapt/issues/91","labels_url":"https://api.github.com/repos/newca12/gapt/issues/91/labels{/name}","comments_url":"https://api.github.com/repos/newca12/gapt/issues/91/comments","events_url":"https://api.github.com/repos/newca12/gapt/issues/91/events","html_url":"https://github.com/newca12/gapt/issues/91","id":55583634,"number":91,"title":"schematized proofs","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/2%E2%80%935%20stars","name":"2–5 stars","color":"FFFFFF"},{"url":"https://api.github.com/repos/newca12/gapt/labels/Component-LogicalDataStructures","name":"Component-LogicalDataStructures","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-Release4.0","name":"Milestone-Release4.0","color":"FFFFFF"},{"url":"https://api.github.com/repos/newca12/gapt/labels/Priority-High","name":"Priority-High","color":"FFFFFF"},{"url":"https://api.github.com/repos/newca12/gapt/labels/Type-Feature","name":"Type-Feature","color":"FFFFFF"}],"state":"open","locked":false,"assignee":null,"milestone":null,"comments":7,"created_at":"2015-01-27T07:10:26Z","updated_at":"2015-01-27T07:11:00Z","closed_at":null,"body":"_From [fra...@gmail.com](https://code.google.com/u/108596877348066494139/) on November 24, 2010 15:42:32_\n\nFor the ASAP project, we will want to support schematized proofs and algorithms on them in the future.\r\n\r\nIn particular, schematized proofs will contain \"proof links\" to other proof definitions, maybe even to the same proof definition with a different index (e.g. we define a proof p(i) and in the definition of the proof, we reference p(i-1)).\r\n\r\nOne possibility to implement this would be to have a proof database collecting names and indices of proofs, and a \"prooflink rule\" which references the name and the index. An algorithm can then query the database for the proof definition.\n\n_Original issue: http://code.google.com/p/gapt/issues/detail?id=91_"},"comment":{"url":"https://api.github.com/repos/newca12/gapt/issues/comments/71599271","html_url":"https://github.com/newca12/gapt/issues/91#issuecomment-71599271","issue_url":"https://api.github.com/repos/newca12/gapt/issues/91","id":71599271,"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-27T07:11:00Z","updated_at":"2015-01-27T07:11:00Z","body":"_From [fra...@gmail.com](https://code.google.com/u/108596877348066494139/) on August 23, 2011 07:14:18_\n\nPreliminary implementation completed.\r\n\r\nFormula schemata: at.logic.language.schema\r\nProof schemata: at.logic.calculi.slk\r\n\r\nProof schemata are pairs of \"SLK\" proofs (basically LK + rules for Formula schemata + proof links).\r\n\r\nAlogrithms for computing the characteristic clause set can be found in at.logic.transformations.ceres.\n\n**Status:** Fixed  \n**Labels:** -Type-Enhancement -Priority-Low Type-Feature Priority-High  \n"}}