{"entities":{"Q3088022":{"pageid":3098737,"ns":120,"title":"Item:Q3088022","lastrevid":51317651,"modified":"2026-01-17T17:56:17Z","type":"item","id":"Q3088022","labels":{"en":{"language":"en","value":"Composable discovery engines for interactive theorem proving"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5940081"}},"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":"Q3088022$28C93A92-D090-44FC-8397-0E6595563672","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"9e7efc35c838f04cf38975fd895793985625ea75","datavalue":{"value":{"text":"Composable Discovery Engines for Interactive Theorem Proving","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q3088022$253BE999-871D-4664-A056-378F72655456","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"b26f485e19d558010c22e9c26db97ece0d8bb4e5","datavalue":{"value":"1342.68302","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3088022$E222287E-1955-4F84-BEC1-CDEB68EFF52E","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"391b1c14a96ce80a6ed990fb17a01c999bacab16","datavalue":{"value":"10.1007/978-3-642-22863-6_28","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3088022$E599DA76-EA41-4D8C-A879-294C7371A60E","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"4cb07b0f36245cb0e201fcad66e2b3ffb9cccb83","datavalue":{"value":{"entity-type":"item","numeric-id":2907336,"id":"Q2907336"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3088022$3B3B2060-E107-44EA-B3B8-90B901C1ED77","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"8d78e8b1fd2bada0896418639974db329feb4fe3","datavalue":{"value":{"entity-type":"item","numeric-id":2102945,"id":"Q2102945"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3088022$67038A0A-DBF9-4077-B593-32CC955F5FBE","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"d43c6ce6e92d67a2cb7e4a7df2a7d5eeec36e724","datavalue":{"value":{"entity-type":"item","numeric-id":2829237,"id":"Q2829237"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3088022$69421BA2-49F1-4F49-9D8A-2FE7911DF160","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"cf253edeced6fad2edf52e73f99001914b4fc105","datavalue":{"value":{"time":"+2011-08-17T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q3088022$648EFD50-5F40-4409-8860-6C9FAD658C76","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3088022$9E36295E-97B7-4EAB-B3B5-5444D108383C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"159426a5937e62cfbbcc198dd4848ab52d6e715e","datavalue":{"value":"68U05","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3088022$4119862C-5496-42FB-B96D-B532D5FCE453","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"502251653148827497390a12277ba861f511e573","datavalue":{"value":"5940081","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3088022$CDFC56AF-A522-4B82-B7FC-0DCA7E213F0A","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":"Q3088022$6EAA79D0-FBC7-4D57-A4C5-4B458D2C302E","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":"Q3088022$8B32A9E4-C475-4A4E-A5BA-E0333E31B19F","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":"Q3088022$477A20F5-7047-4779-8EBD-0582744F28E2","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"eb3e535cf6e77f55bec6beda0758ef0a0960fc91","datavalue":{"value":"https://doi.org/10.1007/978-3-642-22863-6_28","type":"string"},"datatype":"url"},"type":"statement","id":"Q3088022$6E8B8DEE-F81E-4105-A36A-E2C4608F7CF1","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"1ea134c8c3a99e94197901751f1ae8b6a8409275","datavalue":{"value":"W2139827631","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3088022$3E5D9DE2-352A-4215-9C57-EDAC6E8D755F","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"5f84acc216b46a16d3a5b1ae053e7c59afca67c6","datavalue":{"value":{"entity-type":"item","numeric-id":5437031,"id":"Q5437031"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3088022$5C8D801C-B9A0-4C95-9E67-7D7D4ECE1173","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c00ecccc176b971f8f655f17f279ab75b6423f0b","datavalue":{"value":{"entity-type":"item","numeric-id":2432769,"id":"Q2432769"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3088022$371A8790-EA1A-4BB9-99B1-B8169CE2A823","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a10bbeb6c6903ace983b2dbf286a2ef4e5b248ab","datavalue":{"value":{"entity-type":"item","numeric-id":1331625,"id":"Q1331625"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3088022$F18AAA65-0D3C-4C93-BCF9-F063DCDE5C2C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"dd16ae4cad5f71d0d556fbc58f8ff4114408f448","datavalue":{"value":{"entity-type":"item","numeric-id":5166623,"id":"Q5166623"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3088022$F25508E5-02DC-4FC8-9898-83C13FB22872","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"74be213fb432601c8f7cbf47c2a19a1cc59373c3","datavalue":{"value":{"entity-type":"item","numeric-id":3638924,"id":"Q3638924"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3088022$19E02800-9533-4F2D-B4C0-726CA4624FA6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"502ad8224b7ee39a96e36cfcfba1b8b740baa8c6","datavalue":{"value":{"entity-type":"item","numeric-id":4790672,"id":"Q4790672"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3088022$9C65DF2C-F2B4-4E5F-BE38-E294368FEA20","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"115dac803297c03ade9b4e26c7469cff96ceaf3f","datavalue":{"value":{"entity-type":"item","numeric-id":2907337,"id":"Q2907337"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a92161fe2208d084af7b8e09805ab9fecb46e095","datavalue":{"value":{"amount":"+0.7953840494155884","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":"Q3088022$38755E13-7CA0-4F59-AD5F-5CE8979199E0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"17d9afcf606fbc318ea0644e73863cd301aaf85f","datavalue":{"value":{"entity-type":"item","numeric-id":3102743,"id":"Q3102743"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6796cabe20a7bc84c2b5d252658effb6c5109a9d","datavalue":{"value":{"amount":"+0.7454999685287476","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":"Q3088022$B7792B6D-D7D5-4C82-9A76-83DE59C0E504","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d31ac5b611e1dc394bc6dbb9071cf4d1998a3862","datavalue":{"value":{"entity-type":"item","numeric-id":4524769,"id":"Q4524769"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"50065615cf4e3da0e1cbb8384f5fc753a53487d4","datavalue":{"value":{"amount":"+0.7343950271606445","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":"Q3088022$BAF6127A-F371-4488-8ECD-954F3485E23D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1dfa61574fc575acc4cb7d0ca05a72ef1b08a526","datavalue":{"value":{"entity-type":"item","numeric-id":2287904,"id":"Q2287904"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e6e40d700ba282be8711a59601f51203ace6d8b1","datavalue":{"value":{"amount":"+0.7287039756774902","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":"Q3088022$BF402E8C-5165-4956-AC13-634A60A0C524","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9f8b671d2377fddf734ddb65ec2e118032724f1a","datavalue":{"value":{"entity-type":"item","numeric-id":1687709,"id":"Q1687709"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"59a7455ec7acb6d69a3ef961db515f43c644ba75","datavalue":{"value":{"amount":"+0.7247725129127502","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":"Q3088022$3A3E61D6-9829-4DF2-98D7-B5FF018AE18F","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:3088022","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:3088022"}}}}}