Reasoning with database #1836

eugenk · 2018-02-26T09:44:18Z

This should add database support for reasoning. It changes the REST API wrt. Proving/Consistency-Checking.

Please 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.

REST API

POST /prove/coded-iri/command-list is for invoking a prover on a proof goal. It accepts the following request body

{
  "format": "json", // or "xml" or "db" //optional
  "goals": [ // required
    {
      "node": "Nat__E1", // required
      "conjecture": "ga_comm___+__", // optional, if left out, every conjecture will be proved on its own with this configuration
      "reasonerConfiguration": { // required
        "timeLimit": 10, // seconds // required
        "reasoner": "EProver" // optional
      },
      "premiseSelection": { // optional
        "kind": "manual", // or "sine" // required
        "manualPremises": ["Ax1", "Ax2"], // required if kind is "manual"
        "sineDepthLimit": 5, // optional (default: unlimited)
        "sineTolerance": 1.7, // optional (default: 1.0)
        "sinePremiseNumberLimit": 50 // optional (default: unlimited)
      },
      "useTheorems": true, // use previously proven goals as axioms // optional (default: true)
      "printDetails": true, // print details of the proof in xml/json output // optional (default: true)
      "printProof": true // print the prover output in xml/json output // optional (default: true)
    }
  ]
}

Example call with curl:

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)"

POST /consistency-check/coded-iri/command-list is for invoking a consistency-checker on a node. It accepts the following request body

{
  "format": "json", // or "xml" or "db" //optional
  "goals": [ // required
    {
      "node": "Nat__E1", // required
      "reasonerConfiguration": { // required
        "timeLimit": 10, // seconds // required
        "reasoner": "darwin" // optional
      },
      "useTheorems": true, // use previously proven goals as axioms // optional (default: true)
    }
  ]
}

Example call with curl:

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)"

To Do

Refactor buildReasoningCache. See Reasoning with database #1836 (comment). Done in 0d3de41.
Remove the parameterize call of logic translations. See Reasoning with database #1836 (comment) for the required escaping and a few comments above that one for the general problem. Done in a different way in 957a8be.
Completely change the Sentence/LocIdBase structure. See Reasoning with database #1836 (comment) for a possible solution.
- Adjust the database schema
- Save OMSLocIdSentence objects for all imported and non-imported sentences
- Fetch the correct sentence from the database during reasoning.

tillmo · 2018-02-26T09:54:33Z

when compiling, I get a number of "missing module" warnings. I am just curious why missing modules do not cause errors. Have you employed some dynamic loading of modules at run-time?

WARNING in hptSomeThingsBelowUs
  missing module Persistence.Schema.ReasoningStatusOnConjectureType
  Probable cause: out-of-date interface files
WARNING in hptSomeThingsBelowUs
  missing module Persistence.Schema.ReasoningStatusOnReasoningAttemptType
  Probable cause: out-of-date interface files
WARNING in hptSomeThingsBelowUs
  missing module Persistence.Schema.ReasoningStatusOnConjectureType
  Probable cause: out-of-date interface files
WARNING in hptSomeThingsBelowUs
  missing module Persistence.Schema.ReasoningStatusOnReasoningAttemptType
  Probable cause: out-of-date interface files
[837 of 866] Compiling Driver.WriteFn   ( Driver/WriteFn.hs, Driver/WriteFn.o ) [Persistence.LogicGraph changed]
WARNING in hptSomeThingsBelowUs
  missing module Persistence.Schema.ReasoningStatusOnConjectureType
  Probable cause: out-of-date interface files
WARNING in hptSomeThingsBelowUs
  missing module Persistence.Schema.ReasoningStatusOnReasoningAttemptType
  Probable cause: out-of-date interface files
[839 of 866] Compiling Persistence.Reasoning ( Persistence/Reasoning.hs, Persistence/Reasoning.o )
[862 of 866] Compiling PGIP.Server      ( PGIP/Server.hs, PGIP/Server.o )
WARNING in hptSomeThingsBelowUs
  missing module Persistence.Schema.ReasoningStatusOnConjectureType
  Probable cause: out-of-date interface files
WARNING in hptSomeThingsBelowUs
  missing module Persistence.Schema.ReasoningStatusOnReasoningAttemptType
  Probable cause: out-of-date interface files

eugenk · 2018-02-26T09:55:33Z

This is because of some left-overs that GHC hasn't detected. make clean should make that go away.

tillmo · 2018-02-26T10:00:29Z

good, thanks. Now I have tried your example call and get:

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)"
*** Error:
user error (no cons checker found)

This is strange because 1) I have tried to prove, not to cons-check, 2) I have cons checkers available when using the old Hets GUI.

eugenk · 2018-02-26T10:01:49Z

Is EProver a valid cons-checker?

tillmo · 2018-02-26T10:11:19Z

no

tillmo · 2018-02-26T10:12:47Z

OK, will try with "prove"

eugenk · 2018-02-26T10:13:07Z

Then it is filtered away in

Hets/PGIP/Server.hs

Lines 1839 to 1847 in c7bf6ef

    
           findConsChecker :: Maybe String -> G_sublogics -> Maybe String 
        
                           -> IO (G_cons_checker, AnyComorphism) 
        
           findConsChecker translationM gSublogic consCheckerNameM = do 
        
             consList <- getFilteredConsCheckers translationM gSublogic 
        
             let findCC x = filter ((== x ) . getCcName . fst) consList 
        
                 consCheckersL = maybe (findCC "darwin") findCC consCheckerNameM 
        
             case consCheckersL of 
        
                   [] -> fail "no cons checker found" 
        
                   (gConsChecker, comorphism) : _ -> return (gConsChecker, comorphism)

which is quite old Hets-code (just moved out into a separate function)

tillmo · 2018-02-26T11:12:38Z

OK, I managed to prove a goal and found the prover output in table reasoner_outputs. I also managed to check consistency of an OMS. However, I did not find the output of the consistency checker in the DB.

tillmo

I will be offline soon, therefore just one comment for now.

tillmo · 2018-02-26T11:30:18Z

PGIP/GraphQL/Result/Action.hs

+
+data Action = Action { evaluationState :: String
+                     , message :: Maybe String
+                     } deriving (Show, Typeable, Data)


why is this datatype called Action? It seems to be more a datatype for storing results of some action?

This might be extended to the action datatype that Tim described in his master's thesis. It can get an ETA and more information about the action in the future.

good, then please add a corresponding comment.

eugenk · 2018-02-26T12:04:12Z

I did not find the output of the consistency checker in the DB.

That's because Hets does not capture the output in the old function consNode.

Hets/PGIP/Server.hs

Lines 1821 to 1837 in c7bf6ef

    
           consNode :: LibEnv -> LibName -> DGraph -> (Int, DGNodeLab) 
        
             -> G_sublogics -> Bool -> Maybe String -> Maybe String -> Maybe Int 
        
             -> ResultT IO (LibEnv, [ProofResult]) 
        
           consNode le ln dg nl@(i, lb) subL useTh mp mt tl = do 
        
             (cc, c) <- liftIO $ findConsChecker mt subL mp 
        
             lift $ do 
        
               cstat <- consistencyCheck useTh cc c ln le dg nl $ fromMaybe 1 tl 
        
               -- Consistency Results are stored in LibEnv via DGChange object 
        
               let cSt = sType cstat 
        
                   le'' = if cSt == CSUnchecked then le else 
        
                          Map.insert ln (changeDGH dg $ SetNodeLab lb 
        
                            (i, case cSt of 
        
                                  CSInconsistent -> markNodeInconsistent "" lb 
        
                                  CSConsistent -> markNodeConsistent "" lb 
        
                                  _ -> lb)) le 
        
               return (le'', [(" ", drop 2 $ show cSt, show cstat, 
        
                               AbsState.ConsChecker cc, c, Nothing)])

tillmo · 2018-02-26T12:18:09Z

OK, but could you then please create an issue for that?

tillmo · 2018-02-26T12:30:53Z

PGIP/Server.hs

+              then case reasoningParametersE of
+                     Left _ -> False
+                     Right _ -> True
+              else True


shorter:
not (validReasoningParams = elem newIde ["prove", "consistency-check"]) || Data.Either.isRight reasoningParametersE
or even
Data.Either.isRight reasoningParametersE <= (validReasoningParams = elem newIde ["prove", "consistency-check"])
Here, <= is read as "if", i.e. reverse "implies". See also https://mail.haskell.org/pipermail/libraries/2016-January/026565.html

tillmo · 2018-02-26T12:42:20Z

PGIP/Server.hs

+
+    isLeft :: Either a b -> Bool
+    isLeft (Left _) = True
+    isLeft _ = False


this function is already provided by Data.Either

tillmo · 2018-02-26T12:44:34Z

PGIP/Server.hs

+
+    unRight :: Either a b -> b
+    unRight (Right x) = x
+    unRight _ = error "PGIP.Server.unRight received a Left."


shorter: unRight = fromRight $ error "PGIP.Server.unRight received a Left."
Perhaps you could make the error message a bit more informative?

I cannot use fromRight. It could not be found even though I have imported Data.Either.

eugenk · 2018-02-26T12:44:56Z

OK, but could you then please create an issue for that?

I think I added it in 0555999.

tillmo · 2018-02-26T12:52:12Z

yes, works, great!

tillmo · 2018-02-26T12:58:11Z

PGIP/Server.hs

+    failOnLefts reasoningCache =
+      let lefts_ = filter isLeft reasoningCache
+      in  if null lefts_
+          then return ()


shorter: if null $ lefts reasoningCache

aha, or better: let lefts_ = lefts reasoningCache

tillmo · 2018-02-26T13:00:44Z

PGIP/Server.hs

+reasonREST opts libEnv libName dGraph_ proverMode location reasoningParameters = do
+  reasoningCacheE <- liftIO $ buildReasoningCache
+  failOnLefts reasoningCacheE
+  let reasoningCache1 = map unRight $ filter (not . isLeft) reasoningCacheE


shorter: let reasoningCache1 = rights reasoningCacheE
(you already know that there are only Right elements)

tillmo · 2018-02-26T13:35:41Z

PGIP/Server.hs

+      )
+      [] $
+      groupBy (\ a b -> ReasoningParameters.node a == ReasoningParameters.node b) $
+        ReasoningParameters.goals reasoningParameters


I find it hard to review buildReasoningCache. Could you please give names to the anonymous functions (even if this means passing more arguments around), and also to the groupby term at the end?

Will do. Could take me some time because I'm working on a different task right now.

tillmo · 2018-02-26T13:40:55Z

PGIP/Server.hs

+              Nothing ->
+                fail ("Cannot compute global theory of: "
+                      ++ showName (dgn_name nodeLabel) ++ "\n")
+              Just gTheory_ -> return gTheory_


this is a repetition of lines 1898ff. Could be relegated into a small function.

tillmo · 2018-02-26T13:42:16Z

PGIP/Server.hs

+              Nothing ->
+                fail ("Cannot compute global theory of: "
+                      ++ showName (dgn_name nodeLabel) ++ "\n")
+              Just gTheory_ -> return gTheory_


this is a repetition of lines 1898ff. Could be relegated into a small function.

jelmd · 2018-02-26T13:48:00Z

BTW: In Issue ??? you asked for DB "driver" separation as done for MySQL. This would at least in theory allow a "no DB at all" configuration. So related questions are: Is that a supported config? If so, is the new code prepared for it (i.e. relevant parts enclosed in e.g. #ifdef USE_DB ... #endif )?

eugenk · 2018-02-26T13:48:46Z

It is compatible to a no-db configuration.

eugenk · 2018-02-26T13:51:28Z

The relevant code is only called if Hets has been called with database-related commandline-options.

tillmo · 2018-02-26T14:51:16Z

I have a question about logic_translations. When I prove a simple first-order goal with a TPTP prover like SPASS, in the json I get

 "used_translation": "CASL2SoftFOL",

In the DB, I get

INSERT INTO "logic_translations" VALUES(1,'id-casl-condEq-casl2softfol');

How can a comorphism be reconstructed from id-casl-condEq-casl2softfol'? After all, this comorphism has two constituents, but the name uses three dashes.

EDIT: the problem should be even worse with

INSERT INTO "logic_translations" VALUES(2,'id-casl-condEq-casl2tptp-fof');

because id-casl-condEq-casl2tptp-fof cannot be split into its constituents by simple parsing.

tillmo · 2018-02-26T15:04:04Z

The last question is relevant when I want to specify a translation (possibly a composition of logic mappings) that should be used for proving. Now my question is: how can I do this? I tried

till@mark:~/projects/Hets$ curl -X POST -H "Content-Type: application/json" -d '{"format": "db", "goals": [{"node": "sp", "conjecture": d=c", "reasonerConfiguration": {"timeLimit": 10, "reasoner": "SPASS"}, "translation": "casl2softfol", "premiseSelection": {"kind": "sine", "sineDepthLimit": 2, "sineTolerance": 1, "sinePremiseNumberLimit": 50}}]}' "localhost:8000/prove/$(urlencode /home/till/temp/prove.dol)/auto/full-theories/full-signatures?hets-libdirs=$(urlencode $HETS_LIB)"
*** Error:
user error (No matching translation or prover found for sp
)
till@mark:~/projects/Hets$ curl -X POST -H "Content-Type: application/json" -d '{"format": "db", "goals": [{"node": "sp", "conjecture": d=c", "reasonerConfiguration": {"timeLimit": 10, "reasoner": "SPASS"}, "translation": "CASL2SOFTFOL", "premiseSelection": {"kind": "sine", "sineDepthLimit": 2, "sineTolerance": 1, "sinePremiseNumberLimit": 50}}]}' "localhost:8000/prove/$(urlencode /home/till/temp/prove.dol)/auto/full-theories/full-signatures?hets-libdirs=$(urlencode $HETS_LIB)"
*** Error:
user error (No matching translation or prover found for sp
)

By the way, the error message would be more informative if the translation or prover that has not been found were included into the message.

tillmo · 2018-02-26T15:17:09Z

It seems to be that only Persistence.LogicGraph.findLogicMappingBySlug can find a logic mapping, given a string. However, this function assumes that the logic mapping is already stored in the database. What if the user specifies a logic mapping (with several constituents) not present in the database, to be used for proving?

tillmo · 2018-02-26T15:31:05Z

There seems to be problem with imported axioms. Consider

spec sp =
  sort s
  ops a,b,c:s
  . a=b %(a=b)%
  . b=c %(b=c)%
end

spec sp1 =
sp then
  . a=c %(a=c)% %implied
end

I get

curl -X POST -H "Content-Type: application/json" -d '{"format": "db", "goals": [{"node": "sp1", "conjecture": "a=c", "reasonerConfiguration": {"timeLimit": 10, "reasoner": "SPASS"}, "premiseSelection": {"kind": "sine", "sineDepthLimit": 2, "sineTolerance": 1, "sinePremiseNumberLimit": 50}}]}' "localhost:8000/prove/$(urlencode /home/till/temp/prove3.dol)/auto/full-theories/full-signatures?hets-libdirs=$(urlencode $HETS_LIB)"
*** Error:
Persistence.Reasoning.saveToDatabase: Could not find Sentence file:///home/till/temp/prove3.dol//oms/sp1/sentences/a=b

although the sentence is there (but for OMS sp, not sp1!)

INSERT INTO "sentences" VALUES(41,36,12,'a=b','. a = b');
INSERT INTO "oms" VALUES(36,35,18,80,2,NULL,6,NULL,NULL,NULL,NULL,'dg_basic_spec',9,11,'sp','sp','',0,0,0,'Open');
INSERT INTO "oms" VALUES(43,35,19,80,2,NULL,7,NULL,NULL,NULL,NULL,'dg_basic_spec',10,14,'sp1','sp1','',0,0,0,'Open');
C

tillmo · 2018-02-26T15:35:07Z

Persistence/Reasoning.hs

+            let goalName = fromJust $ rceGoalNameM reasoningCacheGoal
+            performPremiseSelection opts gTheory goalName
+              premiseSelectionParameters premiseSelectionKindV
+


I would omit this blank line, or else also add one before the returnbelow.

tillmo · 2018-04-07T13:09:32Z

Note that the origin of sentences is now available, see #1837

eugenk · 2018-04-07T13:40:33Z

I still would like to fix the origin in another pull request. I'm not sure if I should do something about travis not finishing for PostgreSQL. It will be difficult though, because recreating the cache and compiling consumes almost the whole time quota.

tillmo · 2018-04-07T17:43:06Z

OK, then I suggest to merge this now.

luisenriqueramos1977 · 2021-02-06T15:16:34Z

Hi, I am having the issue:
*** Error: no matching translation or prover found, when I try to prove an specification where an axiom is imported like the example commented by tillmo on 26 Feb 2018.
I wonder if there is a solution for such issue?.

Luis Ramos

eugenk requested a review from tillmo February 26, 2018 09:44

tillmo reviewed Feb 26, 2018

View reviewed changes

Till Mossakowski and others added 20 commits April 7, 2018 14:51

made coercion type safe

884441f

Remove commented code.

b0ae3c8

Re-implement proving for the REST interface.

429b556

Cleanup.

7644114

Fix SInE selection.

1feb238

Cleanup.

b14403d

Fix SInE.

6069ca3

Fix provers command.

318bd12

Fix column name.

6fed14b

Remove commented out code.

bc3c08f

Capture consistency checker output.

5edab76

Obey Review.

042b90e

Obey review.

ba92469

Obey Review.

bc8ed1b

Refactor buildReasoningCache.

c6abde8

Add name to LogicTranslation and get rid of compiler warnings.

36f5aa8

Save all sentences in the database instead of only local ones.

15cfa08

Rename column to make it more compact.

71b7829

Add name to LogicInclusion.

d462b80

Save used sentences of a proof attempt.

f4873e7

eugenk force-pushed the reasoning_with_database branch from 16f270a to f4873e7 Compare April 7, 2018 13:35

eugenk merged commit abdc8c3 into master Apr 8, 2018

eugenk deleted the reasoning_with_database branch April 8, 2018 08:52

eugenk mentioned this pull request Apr 15, 2018

Add used_sentences association to ProofAttempt. ontohub/ontohub-models#180

Merged

This was referenced Jan 19, 2019

Receive and perform proving/consistency checking commands ontohub/hets-agent#103

Open

Send proving/consistency checking commands to RabbitMQ ontohub/ontohub-backend#493

Open

Reasoning with database #1836

Reasoning with database #1836

Conversation

eugenk commented Feb 26, 2018 • edited Loading

REST API

To Do

tillmo commented Feb 26, 2018

eugenk commented Feb 26, 2018 • edited Loading

tillmo commented Feb 26, 2018

eugenk commented Feb 26, 2018

tillmo commented Feb 26, 2018

tillmo commented Feb 26, 2018

eugenk commented Feb 26, 2018

tillmo commented Feb 26, 2018

tillmo left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

eugenk commented Feb 26, 2018

tillmo commented Feb 26, 2018

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

eugenk commented Feb 26, 2018

tillmo commented Feb 26, 2018

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

jelmd commented Feb 26, 2018

eugenk commented Feb 26, 2018

eugenk commented Feb 26, 2018

tillmo commented Feb 26, 2018 • edited Loading

tillmo commented Feb 26, 2018

tillmo commented Feb 26, 2018

tillmo commented Feb 26, 2018

Choose a reason for hiding this comment

tillmo commented Apr 7, 2018

eugenk commented Apr 7, 2018

tillmo commented Apr 7, 2018

luisenriqueramos1977 commented Feb 6, 2021

eugenk commented Feb 26, 2018 •

edited

Loading

eugenk commented Feb 26, 2018 •

edited

Loading

tillmo commented Feb 26, 2018 •

edited

Loading