{"action":"created","issue":{"url":"https://api.github.com/repos/spechub/Hets/issues/1641","repository_url":"https://api.github.com/repos/spechub/Hets","labels_url":"https://api.github.com/repos/spechub/Hets/issues/1641/labels{/name}","comments_url":"https://api.github.com/repos/spechub/Hets/issues/1641/comments","events_url":"https://api.github.com/repos/spechub/Hets/issues/1641/events","html_url":"https://github.com/spechub/Hets/issues/1641","id":157741909,"number":1641,"title":"Module extraction does not keep prefixes","user":{"login":"tillmo","id":642775,"avatar_url":"https://avatars.githubusercontent.com/u/642775?v=3","gravatar_id":"","url":"https://api.github.com/users/tillmo","html_url":"https://github.com/tillmo","followers_url":"https://api.github.com/users/tillmo/followers","following_url":"https://api.github.com/users/tillmo/following{/other_user}","gists_url":"https://api.github.com/users/tillmo/gists{/gist_id}","starred_url":"https://api.github.com/users/tillmo/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/tillmo/subscriptions","organizations_url":"https://api.github.com/users/tillmo/orgs","repos_url":"https://api.github.com/users/tillmo/repos","events_url":"https://api.github.com/users/tillmo/events{/privacy}","received_events_url":"https://api.github.com/users/tillmo/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":{"login":"mcodescu","id":1632930,"avatar_url":"https://avatars.githubusercontent.com/u/1632930?v=3","gravatar_id":"","url":"https://api.github.com/users/mcodescu","html_url":"https://github.com/mcodescu","followers_url":"https://api.github.com/users/mcodescu/followers","following_url":"https://api.github.com/users/mcodescu/following{/other_user}","gists_url":"https://api.github.com/users/mcodescu/gists{/gist_id}","starred_url":"https://api.github.com/users/mcodescu/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/mcodescu/subscriptions","organizations_url":"https://api.github.com/users/mcodescu/orgs","repos_url":"https://api.github.com/users/mcodescu/repos","events_url":"https://api.github.com/users/mcodescu/events{/privacy}","received_events_url":"https://api.github.com/users/mcodescu/received_events","type":"User","site_admin":false},"milestone":null,"comments":9,"created_at":"2016-05-31T18:43:59Z","updated_at":"2016-06-02T08:30:09Z","closed_at":null,"body":"When I prove the goal in the file below using SPASS, I get\r\n```\r\nhets: SuleCFOL2SoftFOL.transPREDSYMB: unknown pred: Qual_pred_name A (Pred_type [Thing] nullRange) nullRange\r\n```\r\n\r\n```\r\n%prefix( : <http://www.omg.org/spec/DOL/DOL-terms/> )%\r\n\r\nlogic OWL\r\n\r\nontology O1 = \r\n  Class: A SubClassOf: B\r\n  Class: B SubClassOf: C\r\n  Class: C\r\n  Class: D\r\n  extract A, C\r\nend\r\n\r\nontology O2 = \r\nClass: C \r\nClass: A SubClassOf: C \r\n\r\nend \r\n\r\ninterpretation int : O2 to O1 end\r\n```\r\n\r\nNote that the following works, showing that it must be related to module extraction:\r\n```\r\n%prefix( : <http://www.omg.org/spec/DOL/DOL-terms/> )%\r\n\r\nlogic OWL\r\n\r\nontology O1 = \r\n  Class: A SubClassOf: B\r\n  Class: B SubClassOf: C\r\n  Class: C\r\nend\r\n\r\nontology O2 = \r\nClass: C \r\nClass: A SubClassOf: C \r\n\r\nend \r\n\r\ninterpretation int : O2 to O1 end\r\n```\r\nIndeed, the source of the problem seems to be that the default prefix for the module is not that of the larger ontology. As a consequence, symbols A and C without prefix (ocurring in the proof goal) cannot be found in the signature."},"comment":{"url":"https://api.github.com/repos/spechub/Hets/issues/comments/223228365","html_url":"https://github.com/spechub/Hets/issues/1641#issuecomment-223228365","issue_url":"https://api.github.com/repos/spechub/Hets/issues/1641","id":223228365,"user":{"login":"tillmo","id":642775,"avatar_url":"https://avatars.githubusercontent.com/u/642775?v=3","gravatar_id":"","url":"https://api.github.com/users/tillmo","html_url":"https://github.com/tillmo","followers_url":"https://api.github.com/users/tillmo/followers","following_url":"https://api.github.com/users/tillmo/following{/other_user}","gists_url":"https://api.github.com/users/tillmo/gists{/gist_id}","starred_url":"https://api.github.com/users/tillmo/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/tillmo/subscriptions","organizations_url":"https://api.github.com/users/tillmo/orgs","repos_url":"https://api.github.com/users/tillmo/repos","events_url":"https://api.github.com/users/tillmo/events{/privacy}","received_events_url":"https://api.github.com/users/tillmo/received_events","type":"User","site_admin":false},"created_at":"2016-06-02T08:30:09Z","updated_at":"2016-06-02T08:30:09Z","body":"Could you please create a pull request for that branch?"}}
{"actor":{"display_login":"tillmo"}}