{"action":"created","issue":{"url":"https://api.github.com/repos/spechub/Hets/issues/1546","labels_url":"https://api.github.com/repos/spechub/Hets/issues/1546/labels{/name}","comments_url":"https://api.github.com/repos/spechub/Hets/issues/1546/comments","events_url":"https://api.github.com/repos/spechub/Hets/issues/1546/events","html_url":"https://github.com/spechub/Hets/issues/1546","id":118996853,"number":1546,"title":"TPTP/THF: No Symbols in Axioms/Theorems","user":{"login":"eugenk","id":339751,"avatar_url":"https://avatars.githubusercontent.com/u/339751?v=3","gravatar_id":"","url":"https://api.github.com/users/eugenk","html_url":"https://github.com/eugenk","followers_url":"https://api.github.com/users/eugenk/followers","following_url":"https://api.github.com/users/eugenk/following{/other_user}","gists_url":"https://api.github.com/users/eugenk/gists{/gist_id}","starred_url":"https://api.github.com/users/eugenk/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/eugenk/subscriptions","organizations_url":"https://api.github.com/users/eugenk/orgs","repos_url":"https://api.github.com/users/eugenk/repos","events_url":"https://api.github.com/users/eugenk/events{/privacy}","received_events_url":"https://api.github.com/users/eugenk/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"milestone":null,"comments":4,"created_at":"2015-11-26T08:35:01Z","updated_at":"2015-11-26T10:49:12Z","closed_at":null,"body":"Hets does not output any Symbols in the Axioms and Theorems for TPTP and THF:\r\n\r\n\r\n\r\n##### TPTP (bad output)\r\n```\r\n$ hets -o xml --full-signatures -a none -v2 -O /tmp/ +RTS -K1G -RTS --full-theories -A https://gist.github.com/eugenk/95b5c14c29f761dac07e/raw/a7ced0926bb6f1b4b0efc6277bbcfba57a680fba/compts_1__t10_compts_1.p --input-type=tptp\r\n$ cat /tmp/compts_1__t10_compts_1.p.xml\r\n<?xml version='1.0' ?>\r\n<DGraph filename=\"https://gist.github.com/eugenk/95b5c14c29f761dac07e/raw/a7ced0926bb6f1b4b0efc6277bbcfba57a680fba/compts_1__t10_compts_1.p\" mime-type=\"text/plain\" libname=\"compts_1__t10_compts_1\" dgnodes=\"1\" dgedges=\"0\" nextlinkid=\"0\">\r\n  <DGNode name=\"https://gist.github.com/eugenk/95b5c14c29f761dac07e/raw/a7ced0926bb6f1b4b0efc6277bbcfba57a680fba/compts_1__t10_compts_1.p\" reference=\"false\" logic=\"SoftFOL\" refname=\"https://gist.github.com/eugenk/95b5c14c29f761dac07e/raw/a7ced0926bb6f1b4b0efc6277bbcfba57a680fba/compts_1__t10_compts_1.p\" relxpath=\"/\">\r\n    <Declarations>\r\n      <Symbol kind=\"sort\" name=\"U\" iri=\"U\">U</Symbol>\r\n      [...]\r\n      <Symbol kind=\"predicate\" name=\"v2_compts_1\" iri=\"v2_compts_1\">v2_compts_1: U * U</Symbol>\r\n    </Declarations>\r\n    <Symbols>\r\n      <Symbol kind=\"sort\" name=\"U\" iri=\"U\">U</Symbol>\r\n      [...]\r\n      <Symbol kind=\"predicate\" name=\"v2_compts_1\" iri=\"v2_compts_1\">v2_compts_1: U * U</Symbol>\r\n    </Symbols>\r\n    <Axioms>\r\n      <Axiom name=\"antisymmetry_r2_hidden\">\r\n        <Text>[...]</Text>\r\n        <AST>[...]</AST>\r\n### Symbols should be here ###\r\n      </Axiom>\r\n      [...]\r\n    </Axioms>\r\n    <Theorems>\r\n      <Theorem status=\"open\" name=\"t10_compts_1\">\r\n        <Text>[...]</Text>\r\n        <AST>[...]</AST>\r\n### Symbols should be here ###\r\n      </Theorem>\r\n    </Theorems>\r\n  </DGNode>\r\n</DGraph>\r\n```\r\n\r\n##### THF (bad output)\r\n```\r\n$ hets -o xml --full-signatures -a none -v2 -O /tmp/ +RTS -K1G -RTS --full-theories -A https://gist.github.com/eugenk/95b5c14c29f761dac07e/raw/a7ced0926bb6f1b4b0efc6277bbcfba57a680fba/ALG294-5.het\r\n$ cat /tmp/ALG294-5.xml\r\n<?xml version='1.0' ?>\r\n<DGraph filename=\"https://gist.githubusercontent.com/eugenk/1e4dcbc0106e5120bb06/raw/8f9ea2860eee9006940ae17bc42c63781c8edc69/ALG294-5.het\" mime-type=\"text/het\" libname=\"ALG2945\" dgnodes=\"1\" dgedges=\"0\" nextlinkid=\"0\">\r\n  <DGNode name=\"ALG2945\" range=\"https://gist.githubusercontent.com/eugenk/1e4dcbc0106e5120bb06/raw/8f9ea2860eee9006940ae17bc42c63781c8edc69/ALG294-5.het:3.1-3.14\" reference=\"false\" logic=\"THF\" refname=\"ALG2945\" relxpath=\"/\">\r\n    <Theorems>\r\n      <Theorem status=\"open\" name=\"cPU_X2310B_pme\" range=\"https://gist.githubusercontent.com/eugenk/1e4dcbc0106e5120bb06/raw/8f9ea2860eee9006940ae17bc42c63781c8edc69/ALG294-5.het:58.13-192.22\">\r\n        <Text>[...]</Text>\r\n        <AST>[...]</AST>\r\n### Symbols should be here ###\r\n      </Theorem>\r\n    </Theorems>\r\n  </DGNode>\r\n</DGraph>\r\n```\r\n\r\n##### CASL (good output)\r\n```\r\n$ hets -o xml --full-signatures -a none -v2 -O /tmp/ +RTS -K1G -RTS --full-theories -A https://gist.github.com/eugenk/95b5c14c29f761dac07e/raw/a7ced0926bb6f1b4b0efc6277bbcfba57a680fba/Subclass.casl\r\n$ cat /tmp/Subclass.xml\r\n<?xml version='1.0' ?>\r\n<DGraph filename=\"https://gist.github.com/eugenk/95b5c14c29f761dac07e/raw/a7ced0926bb6f1b4b0efc6277bbcfba57a680fba/Subclass.casl\" mime-type=\"text/het\" libname=\"Subclass\" dgnodes=\"3\" dgedges=\"2\" nextlinkid=\"2\">\r\n  <DGNode name=\"Subclass\" range=\"https://gist.github.com/eugenk/95b5c14c29f761dac07e/raw/a7ced0926bb6f1b4b0efc6277bbcfba57a680fba/Subclass.casl:1.1-19.3\" reference=\"false\" logic=\"CASL\" refname=\"Subclass\" relxpath=\"/\">\r\n    <Declarations>\r\n      <Symbol kind=\"sort\" name=\"s\" iri=\"s\" range=\"https://gist.github.com/eugenk/95b5c14c29f761dac07e/raw/a7ced0926bb6f1b4b0efc6277bbcfba57a680fba/Subclass.casl:2.8\">sort s</Symbol>\r\n      [...]\r\n    </Declarations>\r\n    <Symbols>\r\n      <Symbol kind=\"sort\" name=\"s\" iri=\"s\" range=\"https://gist.github.com/eugenk/95b5c14c29f761dac07e/raw/a7ced0926bb6f1b4b0efc6277bbcfba57a680fba/Subclass.casl:2.8\">sort s</Symbol>\r\n      [...]\r\n    </Symbols>\r\n    <Axioms>\r\n      <Axiom name=\"transitivity\" range=\"https://gist.github.com/eugenk/95b5c14c29f761dac07e/raw/a7ced0926bb6f1b4b0efc6277bbcfba57a680fba/Subclass.casl:11.20-13.72\">\r\n        <Text>[...]</Text>\r\n### Symbols are here: ###\r\n        <Symbol kind=\"sort\" name=\"s\" iri=\"s\" range=\"https://gist.github.com/eugenk/95b5c14c29f761dac07e/raw/a7ced0926bb6f1b4b0efc6277bbcfba57a680fba/Subclass.casl:13.18\">sort s</Symbol>\r\n        <Symbol kind=\"pred\" name=\"subclass\" iri=\"subclass\" range=\"https://gist.github.com/eugenk/95b5c14c29f761dac07e/raw/a7ced0926bb6f1b4b0efc6277bbcfba57a680fba/Subclass.casl:13.22-13.29\">pred subclass : s * s</Symbol>\r\n        <AST>[...]</AST>\r\n      </Axiom>\r\n      [...]\r\n    </Axioms>\r\n  </DGNode>\r\n  [...]\r\n</DGraph>\r\n```"},"comment":{"url":"https://api.github.com/repos/spechub/Hets/issues/comments/159876915","html_url":"https://github.com/spechub/Hets/issues/1546#issuecomment-159876915","issue_url":"https://api.github.com/repos/spechub/Hets/issues/1546","id":159876915,"user":{"login":"cmaeder","id":6043580,"avatar_url":"https://avatars.githubusercontent.com/u/6043580?v=3","gravatar_id":"","url":"https://api.github.com/users/cmaeder","html_url":"https://github.com/cmaeder","followers_url":"https://api.github.com/users/cmaeder/followers","following_url":"https://api.github.com/users/cmaeder/following{/other_user}","gists_url":"https://api.github.com/users/cmaeder/gists{/gist_id}","starred_url":"https://api.github.com/users/cmaeder/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/cmaeder/subscriptions","organizations_url":"https://api.github.com/users/cmaeder/orgs","repos_url":"https://api.github.com/users/cmaeder/repos","events_url":"https://api.github.com/users/cmaeder/events{/privacy}","received_events_url":"https://api.github.com/users/cmaeder/received_events","type":"User","site_admin":false},"created_at":"2015-11-26T10:49:12Z","updated_at":"2015-11-26T10:49:12Z","body":"I guess `symsOfSen` needs to be implemented properly. (and `sym_of`)"}}