{"entities":{"Q3100210":{"pageid":3110925,"ns":120,"title":"Item:Q3100210","lastrevid":51371699,"modified":"2026-01-17T23:33:53Z","type":"item","id":"Q3100210","labels":{"en":{"language":"en","value":"Modular SMT proofs for fast reflexive checking inside Coq"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5977510"}},"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":"Q3100210$C0823FA2-E835-43CA-BF30-04BDD5A657DB","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"655e1e98f4e3444d0523ad3f15c8de0ce949918f","datavalue":{"value":{"text":"Modular SMT Proofs for Fast Reflexive Checking Inside Coq","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q3100210$635630D6-1C64-4FED-81A8-477134B130E6","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"a8d5ab2b83fc709405b6c29b42ea98c90638e8d9","datavalue":{"value":"1350.68224","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3100210$713B4FA0-0BAC-48FB-91B3-0028BD49DBF8","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"5705ba7c27daaa445da7358b51186546db2d18bf","datavalue":{"value":"10.1007/978-3-642-25379-9_13","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3100210$90A5FA2B-DC96-4045-A583-B81668775A26","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"e9d479f47bb17fd8baafebaf6a1d21c8b3a4ec5a","datavalue":{"value":{"entity-type":"item","numeric-id":1687718,"id":"Q1687718"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3100210$63A05AC0-6354-463A-B9EA-2AFDC42F247B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"51f2140d9c56c370d1aaee6dbbd6f3e7fb54182b","datavalue":{"value":{"entity-type":"item","numeric-id":438979,"id":"Q438979"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3100210$B2E31F9B-D7F1-4754-83CE-ECCC90ABC7AD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"322d1bbf43d96eabe74baa00ad17d618005c3800","datavalue":{"value":{"entity-type":"item","numeric-id":287368,"id":"Q287368"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3100210$7A06D652-FDBA-46F9-913B-9EE74C669DC9","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"19e7468504fbcb9c3a09d3a38cdd67d03e02eec6","datavalue":{"value":{"entity-type":"item","numeric-id":2938035,"id":"Q2938035"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3100210$237FA8F2-154F-40BE-8371-41AB2106CB09","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"6d06d6de084d6566994eb3940381939ab0e2877d","datavalue":{"value":{"time":"+2011-11-22T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q3100210$6CECC475-B203-45AA-B10D-44283E083A57","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3100210$AD88EEF4-9AA0-4C57-9F07-B44DC636E1AF","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"99bcf28e3eef2ca34d6386536371bea29b373ae2","datavalue":{"value":"5977510","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3100210$2EA8FAB5-E185-4188-A29B-E7FEE3FA2A83","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ab6ee58efeeaa685ac2b8ecf828badcfb673e8c7","datavalue":{"value":{"entity-type":"item","numeric-id":12929,"id":"Q12929"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3100210$4255C6C4-2AFD-4677-B86A-21E117CD9908","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"2822825cdea331aa7c0ec2c340c1eb36d62db00b","datavalue":{"value":{"entity-type":"item","numeric-id":17123,"id":"Q17123"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3100210$83EDB187-24A0-40CC-BB9D-592E8FEA83EF","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":"Q3100210$DCA2C2AA-905C-4947-BBE4-BBCF5F047D3B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"43f7c4ee5068daf82f8bffbb0f7510a5f16faf63","datavalue":{"value":{"entity-type":"item","numeric-id":16615,"id":"Q16615"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3100210$693CD99D-1897-4781-A45E-AB8AB5510FE4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"875fd2341d7eaef60a26a549ea0c9adfdf328e2e","datavalue":{"value":{"entity-type":"item","numeric-id":17039,"id":"Q17039"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3100210$AF3F1BEB-08EB-4AC1-B119-5106FEA200FB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"5df14ee9c6f65085bdee53a419634b2235aa5c43","datavalue":{"value":{"entity-type":"item","numeric-id":19326,"id":"Q19326"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3100210$FAA57B02-D7BD-4EC6-A0CA-76646CC3C5A9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"cd543fd49199b1838ba332ea5e7b335fbe6c5a58","datavalue":{"value":{"entity-type":"item","numeric-id":19608,"id":"Q19608"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3100210$CBDF3301-C120-46B4-AC39-B9B32215C678","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"6d1b503d7c8f19634e207574177819c306621855","datavalue":{"value":{"entity-type":"item","numeric-id":17038,"id":"Q17038"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3100210$1E913578-C76C-4560-9BBD-8ED15FBE1833","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"af3b5ddb4818ec81bb9bea3bab4852742bff1bd5","datavalue":{"value":{"entity-type":"item","numeric-id":22101,"id":"Q22101"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3100210$BD2AFF75-4614-4AEB-BBB1-A243F11E4BA0","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":"Q3100210$A9891211-38FB-4FD2-A276-D99F1A1C6096","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"89f7242c4f710ac149dc16e89ed346696304f3ad","datavalue":{"value":"https://doi.org/10.1007/978-3-642-25379-9_13","type":"string"},"datatype":"url"},"type":"statement","id":"Q3100210$F4A672E2-5869-4DE7-96E0-DE6D770AB2FD","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"979e310873b310d65fc67ea8791342a0fd5f9482","datavalue":{"value":"W92909155","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3100210$FCD611B1-7351-4B5B-BD90-2CCE4BCC7ECC","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"bb15445443b7a8677c7ef043ed8530f20d54b0c3","datavalue":{"value":{"entity-type":"item","numeric-id":3100209,"id":"Q3100209"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3100210$71E8016A-0214-4B21-9503-301D91DD72D3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f788536331bb87ba4e75963340b885a6c5e47c5c","datavalue":{"value":{"entity-type":"item","numeric-id":5747643,"id":"Q5747643"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3100210$97CFF6D8-ACC1-4E76-8A48-3D2078597F0B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"20e8225b7fde56abf09e51400675a474f11c4844","datavalue":{"value":{"entity-type":"item","numeric-id":3612435,"id":"Q3612435"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3100210$9270116A-64BE-4491-A280-C705F37A5C49","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"494aa31720bff090f87eabeb86ce7380ba058cbf","datavalue":{"value":{"entity-type":"item","numeric-id":5747649,"id":"Q5747649"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3100210$48AF37AE-B38A-42D9-8D08-3F07171E17A5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"bf927db78b3d3748cf319244fe111ce0ec65c938","datavalue":{"value":{"entity-type":"item","numeric-id":5394603,"id":"Q5394603"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3100210$88CAB5D3-CCE0-4C5E-B0E9-6D6A655DDA42","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d0ecda2530a74fd3b958fc170aad75894016b80e","datavalue":{"value":{"entity-type":"item","numeric-id":3541720,"id":"Q3541720"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3100210$5C9C7F9F-9538-403B-B653-735A8C34E870","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ea96e16b6c447e5438826c7902ec9745c5df66e9","datavalue":{"value":{"entity-type":"item","numeric-id":2848059,"id":"Q2848059"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3100210$C36A91CB-80BB-4D76-BBFA-4D608A249E2A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6da6ded218db8e1aba2fc38982f0c41333c8292d","datavalue":{"value":{"entity-type":"item","numeric-id":4809077,"id":"Q4809077"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3100210$CC23E4F4-FFC8-45D3-B50D-AF92D60E3660","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1daf6c1b27d4e2241acccb436e068cfc4f24ffff","datavalue":{"value":{"entity-type":"item","numeric-id":3546294,"id":"Q3546294"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3100210$CE5BCA0E-022E-497F-9CDB-A05BDD6B353C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d2b783d0052b7f250a9573410e9be2b4624ef11e","datavalue":{"value":{"entity-type":"item","numeric-id":5899057,"id":"Q5899057"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3100210$62206A07-6A8B-4155-B4A0-15063240CE94","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"901ba45472e1a0a3be8b2e40215973355027ef09","datavalue":{"value":{"entity-type":"item","numeric-id":2949209,"id":"Q2949209"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3100210$7CA684C8-693F-4B38-A8CE-F628C12B00E0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9811e0f445518a60fcf8a88a2ec5cd76d23ab843","datavalue":{"value":{"entity-type":"item","numeric-id":5477649,"id":"Q5477649"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3100210$ABB6D887-FF40-4350-A99F-E6A5CBF06838","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f2f77790f3de0e7a5198a8f1c64a8023dd2bee09","datavalue":{"value":{"entity-type":"item","numeric-id":5348912,"id":"Q5348912"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3100210$D4B837A4-6357-4EDA-9919-C875BFD795AD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e6b26606a781175a19b1c8fcba43abdeea964791","datavalue":{"value":{"entity-type":"item","numeric-id":2848688,"id":"Q2848688"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3100210$7F773C55-5764-4334-AEA0-968A9E530537","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d1ff3f699fb32cc9d2c446a339d7f9239ca62cd8","datavalue":{"value":{"entity-type":"item","numeric-id":2723407,"id":"Q2723407"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3100210$98804D6A-87B0-4296-AEE7-DF0C43BDB015","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":"Q3100210$9C8EB8CD-33A1-4B61-B59D-264FEC89B8C8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c5791c716254aa1932faf4df96272562ac819ae0","datavalue":{"value":{"entity-type":"item","numeric-id":5703869,"id":"Q5703869"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3100210$4BAA3B4B-A095-49A9-B8FF-7DCF3153D2DF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"716d170b6d9b095492bf0c2b742ee0dbade5bbe0","datavalue":{"value":{"entity-type":"item","numeric-id":3523178,"id":"Q3523178"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3100210$8C4EFF6B-1508-43AA-B9C5-E64B4743F02C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"14d65f813b7bf62e89eaf2eb886e2ecf258499df","datavalue":{"value":{"entity-type":"item","numeric-id":4221106,"id":"Q4221106"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3100210$DB625E0A-AB5F-49F3-8E7C-54CFD49A052A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e427a3de4ce120fbfba5e22bc0ea204ebacee10a","datavalue":{"value":{"entity-type":"item","numeric-id":2557742,"id":"Q2557742"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3100210$D7C22A1A-04F0-4D03-9AA8-9648A3814644","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"271326b3f6ba4699b8b9534f6c64338c8ddd3a50","datavalue":{"value":{"entity-type":"item","numeric-id":1006729,"id":"Q1006729"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3100210$EF7DA81B-5D1F-4D45-9F50-D0EAA8EEE95C","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"fa0c8580ce4e0cb685d0ff86138835bcfa17cf41","datavalue":{"value":{"entity-type":"item","numeric-id":3100209,"id":"Q3100209"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"798664b19f1b64facf1cc7b28c7816e9855644a4","datavalue":{"value":{"amount":"+0.8653414845466614","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":"Q3100210$8FDBD7FA-DB01-4709-8A80-1A6CDB2B9D37","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8738b00b1ca33051359a5e295052e5443121b0d9","datavalue":{"value":{"entity-type":"item","numeric-id":2164216,"id":"Q2164216"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e14d50514151c4bd80e29613b0b7ea3265404c80","datavalue":{"value":{"amount":"+0.809246301651001","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":"Q3100210$A66A47DB-B484-412E-AEA5-CD4DCFB6D528","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b25840e9689e28a5767a31e8370e4b859c5091dc","datavalue":{"value":{"entity-type":"item","numeric-id":5458346,"id":"Q5458346"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5cbca03bab4a873288b302e285ed49bd2d8aad63","datavalue":{"value":{"amount":"+0.7740172147750854","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":"Q3100210$03EE3C0B-83AF-4902-896F-CFBECFCB627F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d943961f845ca0e5235cda46d1b02c9a1ce4d34f","datavalue":{"value":{"entity-type":"item","numeric-id":5747643,"id":"Q5747643"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f2f24fcf0c4136e9cedb061383f8cea0dcd197b4","datavalue":{"value":{"amount":"+0.7637467980384827","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":"Q3100210$4DC0E1CC-52B3-4098-954A-98FE25E49CDA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1dc4a898c2ce53e9d3b4432ba9d09cae8e716f24","datavalue":{"value":{"entity-type":"item","numeric-id":2441776,"id":"Q2441776"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"caee688251bbc2d70ba3e2eb6ff8af861a319dc8","datavalue":{"value":{"amount":"+0.7421987056732178","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":"Q3100210$A67CDACB-2785-419F-98FE-BC473CEC7CF8","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:3100210","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:3100210"}}}}}