{"entities":{"Q438558":{"pageid":440325,"ns":120,"title":"Item:Q438558","lastrevid":61924608,"modified":"2026-04-11T02:35:14Z","type":"item","id":"Q438558","labels":{"en":{"language":"en","value":"Monotonicity inference for higher-order formulas"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6062056"}},"aliases":{},"claims":{"P31":[{"mainsnak":{"snaktype":"value","property":"P31","hash":"fd5912e4dab4b881a8eb0eb27e7893fef55176ad","datavalue":{"value":{"entity-type":"item","numeric-id":56887,"id":"Q56887"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438558$8B7D5A6C-A3B4-451D-A496-DF80A8F2F27D","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"a1dff9fc5b9e73cb8cc09eec7439cf764afe5c39","datavalue":{"value":{"text":"Monotonicity inference for higher-order formulas","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q438558$68B6FBEF-AA76-4932-AAB3-D982CEE33643","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"d1b896a2ebe64cb2d603686a732acae233dedbce","datavalue":{"value":"1266.03021","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q438558$497DECFE-BBA9-4FCA-9732-389C0B7D7F02","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"42c29c686dffd678d9f155b05a4a1aa93e85953c","datavalue":{"value":{"entity-type":"item","numeric-id":287335,"id":"Q287335"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438558$CC82CD63-18D6-4683-B2C6-3440937AABE1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"bb9a75665101462bc01a2c7426c95f31a74ce050","datavalue":{"value":{"entity-type":"item","numeric-id":438557,"id":"Q438557"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438558$64CCCE83-8B27-4BB2-B5D2-C19F149CD83C","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"b84cc8b5923f45dc86ae69f67f68bf56d7ecfce9","datavalue":{"value":{"entity-type":"item","numeric-id":174771,"id":"Q174771"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438558$88F6727F-3545-4C79-ADB8-A6835C73668C","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"6c7ad691786690cf86127845d28cf47311748286","datavalue":{"value":{"time":"+2012-07-31T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q438558$10D7B463-F318-4D84-B154-B730C3EA8177","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"0e954fc76dca5ae3eb783493cf59fea8366f779b","datavalue":{"value":"The authors investigate possibilities of inferring monotonicity of formulae for higher-order logic. This is mainly motivated by their work on model finding, where monotonicity can help prune search space; it is mentioned that another use of monotonicity is to find finite substructures of infinite models.  A formula \\(t\\) in higher-order logic is monotonic w.r.t.\\ a type variable \\(\\alpha\\) if for all scopes \\(S\\), \\(S'\\) such that \\(S \\leq_{\\alpha} S'\\), if \\(t\\) is satisfiable for \\(S\\) then it is also satisfiable for \\(S'\\). The formula \\(t\\) is antimonotonic w.r.t. \\(\\alpha\\) if its negation is monotonic w.r.t. \\(\\alpha\\).  It is first shown that monotonicity w.r.t.\\ \\(\\alpha\\) is undecidable. Then three calculi for inferring monotonicity are presented. The first calculus is based on tracking equality and quantifiers. The second calculus -- based on tracking sets -- addresses some of the problems the first calculus has. The drawback of this second calculus is that it cannot type set comprehension precisely (as a result it cannot infer, for instance, monotonicity of any of the four type-variables occurring in the associativity law for composition). These problems are addressed in a third calculus which handles set comprehension and bounded quantifications.  The implementation of these calculi in \\texttt{Isabelle}'s model finder \\texttt{Nitpick} is evaluated on the user-supplied theorems from six highly polymorphic \\texttt{Isabelle} theories. The tests show that especially the use of the third calculus leads to considerable speed and precision improvements.","type":"string"},"datatype":"string"},"type":"statement","id":"Q438558$25BD3ECD-6EEE-4274-A5E3-7C67E08BD3FC","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"895d5fc798d777f77a43df1e1b11857e28584cdd","datavalue":{"value":{"entity-type":"item","numeric-id":592080,"id":"Q592080"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438558$E8FA58A8-0ABA-4ABF-AC58-CD77925AB932","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q438558$279E883C-58AF-48E8-ACCC-09887B887592","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"dd8503cb84d44ac2adb520ebbb11872e6dc1ec3b","datavalue":{"value":"03B15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q438558$7CA6E90F-8039-4A68-994F-E5526F9350B6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q438558$0A1572D5-ADE1-4576-9F30-A7B3CD915495","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q438558$43182BD1-BCF9-4A94-A392-683F95F9A51C","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"2d25563da5ba90aa1fe7b6883803ed9ea22d9f22","datavalue":{"value":"6062056","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q438558$EC01F1F2-D41D-4AA7-9735-1C55E20844FF","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"39810ec381ba48fb5861c168391fa7d328efd8b1","datavalue":{"value":"higher-order logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q438558$2E3F6FF8-C8B2-4BF6-9A23-5E3BED64C791","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e1e736ba7e5b127a0c37afaca4a8e9165a984d0c","datavalue":{"value":"model finding","type":"string"},"datatype":"string"},"type":"statement","id":"Q438558$FBC660AA-8E69-4A53-B738-918602CB8E5F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ca5830b9e054ca240b1ee150695772e6c0bd6aa7","datavalue":{"value":"\\texttt{Isabelle/HOL}","type":"string"},"datatype":"string"},"type":"statement","id":"Q438558$832EE9D1-5F11-46A4-9B50-EBF89FDF7908","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"c5fcda2c98ddff866834785339eb37077e5eb1fe","datavalue":{"value":{"entity-type":"item","numeric-id":13212,"id":"Q13212"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438558$89B0856E-E96A-41FD-84AA-FBCD688856D4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"2b02b46847f3d7e3a5825b9484a88607b98dbd14","datavalue":{"value":{"entity-type":"item","numeric-id":13958,"id":"Q13958"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438558$9FB1FAEB-F123-40BF-A394-F0DB7969BCDE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"1aec27d540e360c78ddad230e6e300ced62bdec3","datavalue":{"value":{"entity-type":"item","numeric-id":18433,"id":"Q18433"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438558$62FAAA04-95BA-46AA-962C-D92262668A56","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"fa5dc13872ba1592e71dabc4befba1daea72a8a3","datavalue":{"value":{"entity-type":"item","numeric-id":14275,"id":"Q14275"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438558$61D69D44-0031-4397-902E-DDA1AC142CFE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"7f231912461a4cf859d87b4356c5e2a2037e1e84","datavalue":{"value":{"entity-type":"item","numeric-id":17631,"id":"Q17631"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438558$7BB4F875-6718-4431-945F-A8F33281C687","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"41fc9cdab07636dca04412ef0070f1d13ce58f4d","datavalue":{"value":{"entity-type":"item","numeric-id":19148,"id":"Q19148"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438558$AFD92E17-04C2-4213-BB69-FA8C2C1EC092","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"bcb8668d4342f1ce0eb71100202b248217523f94","datavalue":{"value":{"entity-type":"item","numeric-id":22367,"id":"Q22367"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438558$253ED4E8-3D2B-4247-8362-D065C8DC604E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ecb36fec89ff827cd73a8ca1a85f36a2e419c34e","datavalue":{"value":{"entity-type":"item","numeric-id":13377,"id":"Q13377"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438558$A336BFD3-4CD4-4A25-9703-733EFE2EE33A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ee80fa482e8c030191fc3263e069d0dc0cdf7815","datavalue":{"value":{"entity-type":"item","numeric-id":18672,"id":"Q18672"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438558$6F6FE9FE-81B1-4208-83E0-F4FE1A22095A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"d668101f6ec8ba9deddd8d165379a7bb54a38625","datavalue":{"value":{"entity-type":"item","numeric-id":40948,"id":"Q40948"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438558$66798898-CA3B-4694-BD44-49DE56F302B5","rank":"normal"}],"P1460":[{"mainsnak":{"snaktype":"value","property":"P1460","hash":"57f7fea50d2ce1b39b695c4a1313582eed405e38","datavalue":{"value":{"entity-type":"item","numeric-id":5976449,"id":"Q5976449"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438558$96DB19C4-259B-4254-9DB2-5C641623D86C","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"36b84f33197f3f3a251cf959389a8cb0fe39de29","datavalue":{"value":"https://doi.org/10.1007/s10817-011-9234-1","type":"string"},"datatype":"url"},"type":"statement","id":"Q438558$66DC7228-7C91-47A9-A9BC-FB490F3380AF","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"0242535924cde34d0dcc30714baf426e378d094d","datavalue":{"value":"W2018758446","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q438558$DF595842-4C7C-4BAC-B2AF-071FA9967E24","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"b11646dfc2677d6614fa16128dbbd7844776606d","datavalue":{"value":{"entity-type":"item","numeric-id":1847766,"id":"Q1847766"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438558$D739ABA2-01D5-4A37-B2BE-D0784171F6A4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"20edcd59bc17da043a934bc071def38938532f97","datavalue":{"value":{"entity-type":"item","numeric-id":4945200,"id":"Q4945200"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438558$BD2EBC43-2B56-4AA7-BEC8-E48DF9745B2A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8be5d82ecbcbf9223e0aa9ae73481bbd0db4c55e","datavalue":{"value":{"entity-type":"item","numeric-id":5747753,"id":"Q5747753"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438558$9B9B573B-26A3-4058-9DE2-E2A9C34A9669","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"49023bd5aa461c9f63f0725228815aa2af2e478f","datavalue":{"value":{"entity-type":"item","numeric-id":5747646,"id":"Q5747646"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438558$E98E04FF-9B5A-4B2E-8920-0F1219A83F24","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a1fe080668c047a45e96256ef3b2962fb036501b","datavalue":{"value":{"entity-type":"item","numeric-id":5200026,"id":"Q5200026"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438558$6F0430D2-8A7D-4D06-B48A-B8332CCC4DDD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"df6d745c28f41f3f6887e89cc1ca892988e70309","datavalue":{"value":{"entity-type":"item","numeric-id":5287513,"id":"Q5287513"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438558$5A2D3175-D439-4269-B4BB-BCD345C071BE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b88ce955fc019155ebd9bd8280efa709429c3b2f","datavalue":{"value":{"entity-type":"item","numeric-id":2848413,"id":"Q2848413"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438558$ACE3B81A-FDC4-48B8-96FC-88D50846B84F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ce7b2dd2863358cf2a528999ec6b006fdf400b99","datavalue":{"value":{"entity-type":"item","numeric-id":3899468,"id":"Q3899468"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438558$0C568129-F907-45BF-AD1E-9D86F9F25A1F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7653da84007c7a5f47e587934a232ab2e277182a","datavalue":{"value":{"entity-type":"item","numeric-id":3525136,"id":"Q3525136"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438558$98E163BE-57D7-47F2-9DD3-23AAFF8A0D14","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"84afe353d96a988928bd5d41e96afba7e81d6980","datavalue":{"value":{"entity-type":"item","numeric-id":1600086,"id":"Q1600086"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438558$B8CBCE13-176E-4A03-B439-CA4BCAB5E62E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ac267cefe4c0b3f2d90f4b0252d3226cf35ab665","datavalue":{"value":{"entity-type":"item","numeric-id":1854568,"id":"Q1854568"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438558$CC55966A-8819-4C9D-8A39-A38AE2084109","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"77f4334b25d43b9293350a877e2d317280ca55a9","datavalue":{"value":{"entity-type":"item","numeric-id":3543646,"id":"Q3543646"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438558$B2F5CB13-7A0C-4CFC-AAD3-331B1DE5937D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"28039a446a03faca9d112ce464bbb91b9adbe1ca","datavalue":{"value":{"entity-type":"item","numeric-id":5394160,"id":"Q5394160"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438558$FF024DA5-9095-4B82-AA82-003EB48CF93A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"56e2dbd1c024d492b6dfa954b304f9b8207b1591","datavalue":{"value":{"entity-type":"item","numeric-id":5758136,"id":"Q5758136"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438558$6D4BB934-DC91-4A94-8F02-651FCC68CAFF","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"2e956d20ff72e5a90fcbb34e8426ce6a5cfe0473","datavalue":{"value":"10.1007/S10817-011-9234-1","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q438558$3F26CC2A-7414-4402-B035-4ACD553C3766","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e09b005b504b6e916040423dd9a76490020cc9e9","datavalue":{"value":{"entity-type":"item","numeric-id":5747753,"id":"Q5747753"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5dd127140aeeac1651faebbc9c2eac6d4abcb6d2","datavalue":{"value":{"amount":"+0.9438278079032898","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q438558$9DDFF99E-A3D5-4E31-B0EB-94103C924986","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"24a14c7f8f42b849eccb834d9e52aacec0e68d4a","datavalue":{"value":{"entity-type":"item","numeric-id":4599217,"id":"Q4599217"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"95b2f896e66aaecbd412f82a287bd5932f111acb","datavalue":{"value":{"amount":"+0.706684947013855","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q438558$EDB3B78F-B463-4DA4-AC91-8EDE255106F7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"560f5742f65df3117ea8ed4971289cab4b37e111","datavalue":{"value":{"entity-type":"item","numeric-id":4016555,"id":"Q4016555"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"304fd00c7736740924019e38f0c29d872e8d453f","datavalue":{"value":{"amount":"+0.705437421798706","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q438558$AD1B98A4-22B0-4B31-920F-32A515DFC6EA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c9a6d991b50ee3cacf0f632a65fb75701662b114","datavalue":{"value":{"entity-type":"item","numeric-id":2405244,"id":"Q2405244"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"aebf263d61cb9abf2cce67c6518e8cea5c6e7b9d","datavalue":{"value":{"amount":"+0.7023835778236389","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q438558$86185CF4-E63E-494F-9458-0E60ACD33E60","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"65fc88041f16f9dc16cc8fbfeef56ff32d78e5f1","datavalue":{"value":{"entity-type":"item","numeric-id":5459181,"id":"Q5459181"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9c7bf429576c46ef04439ebf506cfa14be972f4a","datavalue":{"value":{"amount":"+0.6993057131767273","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q438558$0DF5401E-D153-4244-9E0F-B378A0D1DF6D","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Monotonicity inference for higher-order formulas","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Monotonicity_inference_for_higher-order_formulas"}}}}}