{"action":"created","issue":{"url":"https://api.github.com/repos/spechub/Hets/issues/1836","repository_url":"https://api.github.com/repos/spechub/Hets","labels_url":"https://api.github.com/repos/spechub/Hets/issues/1836/labels{/name}","comments_url":"https://api.github.com/repos/spechub/Hets/issues/1836/comments","events_url":"https://api.github.com/repos/spechub/Hets/issues/1836/events","html_url":"https://github.com/spechub/Hets/pull/1836","id":300168739,"number":1836,"title":"Reasoning with database","user":{"login":"eugenk","id":339751,"avatar_url":"https://avatars3.githubusercontent.com/u/339751?v=4","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,"assignees":[],"milestone":null,"comments":37,"created_at":"2018-02-26T09:44:18Z","updated_at":"2018-03-04T16:44:09Z","closed_at":null,"author_association":"CONTRIBUTOR","pull_request":{"url":"https://api.github.com/repos/spechub/Hets/pulls/1836","html_url":"https://github.com/spechub/Hets/pull/1836","diff_url":"https://github.com/spechub/Hets/pull/1836.diff","patch_url":"https://github.com/spechub/Hets/pull/1836.patch"},"body":"This should add database support for reasoning. It changes the REST API wrt. Proving/Consistency-Checking.\r\n\r\nPlease review this carefully because there might be some typos when changing the state (moving through libEnv1, libEnv2, libEnv3 and so on while proving many conjectures). Please also check if there are any logical mistakes like not using the correct gTheory for proving/consistency-checking or not passing the set of all sentences (even imported ones) to the SInE premise selection.\r\n\r\n# REST API\r\n* POST `/prove/coded-iri/command-list` is for invoking a prover on a proof goal. It accepts the following request body\r\n    ```text\r\n    {\r\n      \"format\": \"json\", // or \"xml\" or \"db\" //optional\r\n      \"goals\": [ // required\r\n        {\r\n          \"node\": \"Nat__E1\", // required\r\n          \"conjecture\": \"ga_comm___+__\", // optional, if left out, every conjecture will be proved on its own with this configuration\r\n          \"reasonerConfiguration\": { // required\r\n            \"timeLimit\": 10, // seconds // required\r\n            \"reasoner\": \"EProver\" // optional\r\n          },\r\n          \"premiseSelection\": { // optional\r\n            \"kind\": \"manual\", // or \"sine\" // required\r\n            \"manualPremises\": [\"Ax1\", \"Ax2\"], // required if kind is \"manual\"\r\n            \"sineDepthLimit\": 5, // optional (default: unlimited)\r\n            \"sineTolerance\": 1.7, // optional (default: 1.0)\r\n            \"sinePremiseNumberLimit\": 50 // optional (default: unlimited)\r\n          },\r\n          \"useTheorems\": true, // use previously proven goals as axioms // optional (default: true)\r\n          \"printDetails\": true, // print details of the proof in xml/json output // optional (default: true)\r\n          \"printProof\": true // print the prover output in xml/json output // optional (default: true)\r\n        }\r\n      ]\r\n    }\r\n    ```\r\n    Example call with curl:\r\n    ```text\r\n    curl -X POST -H \"Content-Type: application/json\" -d '{\"format\": \"db\", \"goals\": [{\"node\": \"Nat__E1\", \"conjecture\": \"ga_comm___+__\", \"reasonerConfiguration\": {\"timeLimit\": 10, \"reasoner\": \"EProver\"}, \"premiseSelection\": {\"kind\": \"sine\", \"sineDepthLimit\": 2, \"sineTolerance\": 1, \"sinePremiseNumberLimit\": 50}}]}' \"localhost:8000/consistency-check/$(urlencode $HETS_LIB/Basic/Numbers.casl)/auto/full-theories/full-signatures?hets-libdirs=$(urlencode $HETS_LIB)\"\r\n    ```\r\n* POST `/consistency-check/coded-iri/command-list` is for invoking a consistency-checker on a node. It accepts the following request body\r\n    ```text\r\n    {\r\n      \"format\": \"json\", // or \"xml\" or \"db\" //optional\r\n      \"goals\": [ // required\r\n        {\r\n          \"node\": \"Nat__E1\", // required\r\n          \"reasonerConfiguration\": { // required\r\n            \"timeLimit\": 10, // seconds // required\r\n            \"reasoner\": \"darwin\" // optional\r\n          },\r\n          \"useTheorems\": true, // use previously proven goals as axioms // optional (default: true)\r\n        }\r\n      ]\r\n    }\r\n    ```\r\n    Example call with curl:\r\n    ```text\r\n    curl -X POST -H \"Content-Type: application/json\" -d '{\"format\": \"db\", \"goals\": [{\"node\": \"Nat__E1\", \"reasonerConfiguration\": {\"timeLimit\": 10}}]}' \"localhost:8000/prove/$(urlencode $HETS_LIB/Basic/Numbers.casl)/auto/full-theories/full-signatures?hets-libdirs=$(urlencode $HETS_LIB)\"\r\n    ```\r\n\r\n# To Do\r\n* [x] Refactor `buildReasoningCache`. See https://github.com/spechub/Hets/pull/1836#discussion_r170591991. Done in 0d3de413a.\r\n* [x] Remove the `parameterize` call of logic translations. See https://github.com/spechub/Hets/pull/1836#issuecomment-368876543 for the required escaping and a few comments above that one for the general problem. Done in a different way in 957a8be74.\r\n* [ ] Completely change the Sentence/LocIdBase structure. See https://github.com/spechub/Hets/pull/1836#issuecomment-369156065 for a possible solution.\r\n  * [ ] Adjust the database schema\r\n  * [ ] Save OMSLocIdSentence objects for all imported and non-imported sentences\r\n  * [ ] Fetch the correct sentence from the database during reasoning."},"comment":{"url":"https://api.github.com/repos/spechub/Hets/issues/comments/370243506","html_url":"https://github.com/spechub/Hets/pull/1836#issuecomment-370243506","issue_url":"https://api.github.com/repos/spechub/Hets/issues/1836","id":370243506,"user":{"login":"eugenk","id":339751,"avatar_url":"https://avatars3.githubusercontent.com/u/339751?v=4","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},"created_at":"2018-03-04T16:44:09Z","updated_at":"2018-03-04T16:44:09Z","author_association":"CONTRIBUTOR","body":"Right, Static.ComputeTheory.computeTheory gives me a G_theory with all sentences, but there is no information about the origin of a sentence. My first thought was to simply subtract the local sentences (`dgn_theory nodeLabel`) from the computed theory (`Static.ComputeTheory.computeTheory dGraph nodeId`), but I think this won't work: How do I compare the sentences to decide whether or not to remove them? I cannot compare them by name because they could have been renamed in the import."}}
{"actor":{"display_login":"eugenk"}}