{"entities":{"Q3100204":{"pageid":3110919,"ns":120,"title":"Item:Q3100204","lastrevid":51371690,"modified":"2026-01-17T23:33:51Z","type":"item","id":"Q3100204","labels":{"en":{"language":"en","value":"Formalization of Wu's simple method in Coq"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5977505"}},"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":"Q3100204$091E88D0-C2BA-404A-BA4F-4D8BC34AEE5D","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"4865ceea8534032e4d2286b1ee6d0cf42639bb53","datavalue":{"value":{"text":"Formalization of Wu\u2019s Simple Method in Coq","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q3100204$6B9C9CB8-D517-4A86-B746-5C6E4D8F9966","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"5cf48f4c4d7bf06705ef203a5309b61e905642ce","datavalue":{"value":"1350.68234","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3100204$AAC60278-9F4C-4878-ADCA-40A28F5A4011","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"c51a6a959f3c93d33fecb36eee01482a9a3991af","datavalue":{"value":"10.1007/978-3-642-25379-9_8","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3100204$3CABB6E4-E097-4F96-BC03-6852559B735A","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"bff2af6b003f158d34b8f2e001ab8f1289af7c6b","datavalue":{"value":{"entity-type":"item","numeric-id":3100203,"id":"Q3100203"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3100204$7B6AF626-D2B1-4BC8-AE85-27B768D1E69A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"7154e8ca53ace223b8c5be019b7f4f775aab0292","datavalue":{"value":{"entity-type":"item","numeric-id":294376,"id":"Q294376"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3100204$5BFE3918-32AA-4136-AAEF-FD187758E5FC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"c4f67aad00a911cdfd4a5f73b3962a1f5be1f7e5","datavalue":{"value":{"entity-type":"item","numeric-id":294371,"id":"Q294371"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3100204$64D5A288-D2A4-4F3B-9419-62B1EC2DFCA4","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":"Q3100204$19CDF483-7253-4F92-AF8E-72C3E3158874","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":"Q3100204$579CF04E-67F3-4D1C-A711-97A478078D65","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3100204$EDA0B9DB-1648-4E51-8FB9-061A4BBEC839","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"0ff8b94cef61822418ad82477d6d66bfeedcac9f","datavalue":{"value":"5977505","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3100204$EB77C284-24D4-476D-95C8-A2E81028432E","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d5ef51b89dbf72f7181f6b41896d9233a3e6b1ce","datavalue":{"value":"formalization","type":"string"},"datatype":"string"},"type":"statement","id":"Q3100204$AF836206-93F8-4D66-BBF5-BFB1389CC762","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f7010e5ebaf593fc81efbecd62427d5100a588a3","datavalue":{"value":"automation","type":"string"},"datatype":"string"},"type":"statement","id":"Q3100204$3EFDE5EF-B59E-4853-8632-3779F336A549","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4477c9598ae4965364daa3ce025ec46065fff35c","datavalue":{"value":"geometry","type":"string"},"datatype":"string"},"type":"statement","id":"Q3100204$2326199A-F9B8-491F-B859-DF2F309D9F8A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"58f8cf8243737b642987140e639e60ec078529ee","datavalue":{"value":"Wu's method","type":"string"},"datatype":"string"},"type":"statement","id":"Q3100204$56343CD1-546E-438A-8671-336FE9E556D8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c6a78675f0dcb3af511ac1d4dfa61901e828bcb8","datavalue":{"value":"proof assistant","type":"string"},"datatype":"string"},"type":"statement","id":"Q3100204$D3E43567-C8F3-4EE4-B5A2-F556F3A47FC5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"09e5b68927baf737cf4d5adadb4664c931aae1c2","datavalue":{"value":"Coq","type":"string"},"datatype":"string"},"type":"statement","id":"Q3100204$C307F797-C699-4DD6-B8CD-D6E8008B287A","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"73bf07fb0985efe0166024eb806e5cf2244671a5","datavalue":{"value":{"entity-type":"item","numeric-id":18489,"id":"Q18489"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3100204$26BC7817-2B19-4727-A4D5-1D391E7EAFEF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"97d7cc0b4df8bbc3ba9ede16de8204f49c9583ef","datavalue":{"value":{"entity-type":"item","numeric-id":25527,"id":"Q25527"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3100204$4322909B-A8E1-4801-A935-7186C67E4EE4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"86a4af2bb3c2c33ea624c50ed824f97c07fb9cde","datavalue":{"value":{"entity-type":"item","numeric-id":17876,"id":"Q17876"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3100204$887A2068-0953-4EED-A710-94F99332D7C7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"44711c0dfc3538a7fb734312a1553b4a39dda7da","datavalue":{"value":{"entity-type":"item","numeric-id":13339,"id":"Q13339"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3100204$DD533FB9-D1DD-4EC0-9375-79D849838DE6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"97c52174d6a2c739dccdd83081669a4a937b002e","datavalue":{"value":{"entity-type":"item","numeric-id":15381,"id":"Q15381"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3100204$4836692E-24DB-45C7-9A19-194B05D80F50","rank":"normal"},{"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":"Q3100204$890BD65A-21EF-42F1-B0A5-F6226FC0BBD7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"e5a467e2b8559126e673a21cece3f03b6086929d","datavalue":{"value":{"entity-type":"item","numeric-id":21940,"id":"Q21940"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3100204$5630E3E6-12D5-446A-82E7-77D1EFC586C4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"6a69612fc806d816e598f13eebfec79f0480839d","datavalue":{"value":{"entity-type":"item","numeric-id":18349,"id":"Q18349"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3100204$FD7DF498-0F22-4851-A6B7-C63F18761A3F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"d423aed709d24704c8ca138c3d33e02bafd7a799","datavalue":{"value":{"entity-type":"item","numeric-id":18350,"id":"Q18350"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3100204$CDE1E1F6-641F-4279-ADBC-BC1A4F602DE8","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":"Q3100204$16FD3806-C048-4F24-9C29-339DD09CD80F","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"62d758e2818a6fe246fa1f842b584f77bc0295c7","datavalue":{"value":"https://doi.org/10.1007/978-3-642-25379-9_8","type":"string"},"datatype":"url"},"type":"statement","id":"Q3100204$E3E645D7-1A6C-47EA-8212-EFD4FCAF3C6F","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"71a92a2bf52674c85e1d41429244c36dcfbd0deb","datavalue":{"value":"W120661248","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3100204$30A19D4B-8241-4806-814A-7AC2BA42BB7E","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"f65b705669c63993345434be77161245f32637c5","datavalue":{"value":{"entity-type":"item","numeric-id":3490991,"id":"Q3490991"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3100204$C362885B-E36F-46C3-A711-9697B0D417B7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"509aa10ad44866d9544447fa8185a66eecae22a1","datavalue":{"value":{"entity-type":"item","numeric-id":4264711,"id":"Q4264711"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3100204$9D8016E1-7679-43B7-8984-309C78342266","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b2c6fc65716ca53b4df443be754d1a7c89f6f684","datavalue":{"value":{"entity-type":"item","numeric-id":4857780,"id":"Q4857780"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3100204$4584B543-5417-4009-8CD6-38FE6B530180","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"54eee2313932f532ca016c516cb047dfc95351e0","datavalue":{"value":{"entity-type":"item","numeric-id":5428257,"id":"Q5428257"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3100204$961BDD5F-73D8-4586-9C5A-3FDA172575F4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d8f6392d71399b59cd96cef76735f66148c25250","datavalue":{"value":{"entity-type":"item","numeric-id":3102734,"id":"Q3102734"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3100204$0AB04AF7-156A-4979-B52C-613F748DD13B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c2d8aaacffe81ff9879cd1359153e8aa379e24c6","datavalue":{"value":{"entity-type":"item","numeric-id":5902023,"id":"Q5902023"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3100204$B27763CC-8954-4EFF-A05D-7BD6BD090CF4","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":"Q3100204$A5E09DFE-8739-4C49-A0F6-6DF5AE7A7017","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"50194ca3b7c353b09bf7a69176aa9a9155660faf","datavalue":{"value":{"entity-type":"item","numeric-id":3003228,"id":"Q3003228"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3100204$48176D5B-9420-48CC-9746-4312786D33C3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b7902ad05fc58101eeb009f9da7bcfeb90392bef","datavalue":{"value":{"entity-type":"item","numeric-id":3608762,"id":"Q3608762"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3100204$8C0397D6-5767-422A-962F-5DE29E318982","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a8e615433d7c0da849d212b92d36df1a27bb8523","datavalue":{"value":{"entity-type":"item","numeric-id":3183516,"id":"Q3183516"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3100204$8F5F29D3-D0F7-472D-B711-634D99F4232C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5aa2ae61992a0e5eba0a5e337babaa28b7d7cf92","datavalue":{"value":{"entity-type":"item","numeric-id":437042,"id":"Q437042"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3100204$20D5B557-C1CA-4609-A70C-FA1FBA8BEA57","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"540adcc9e46ea420a940154aee39f09e6ab0a966","datavalue":{"value":{"entity-type":"item","numeric-id":5464649,"id":"Q5464649"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3100204$EA29B5C0-D4FF-48E3-9FB9-AEC09544DC45","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d795b598201d37a3767197b6e0d7bcbc8cde96fc","datavalue":{"value":{"entity-type":"item","numeric-id":2462636,"id":"Q2462636"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3100204$05C81036-9643-4A59-BF1F-945975FAECF8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"aaec4727ba4d5abdc46c7100171bf5ef55ab6706","datavalue":{"value":{"entity-type":"item","numeric-id":583606,"id":"Q583606"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3100204$91963F4A-30AF-4A60-9635-A1F94C695B11","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"57cb6073bb92238a3ac694f94e3d06e7338f0593","datavalue":{"value":{"entity-type":"item","numeric-id":5902031,"id":"Q5902031"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3100204$892FCEAB-FCBA-4B45-A97F-EF744016257F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7ad41095da7320267c1e9f25ef88c7327526f4b8","datavalue":{"value":{"entity-type":"item","numeric-id":3003235,"id":"Q3003235"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3100204$C5C868C5-BCDA-4424-A594-6F9DEFE03EDE","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ef7ee3b7d6d18ddf40be1d05d447cb6374f78511","datavalue":{"value":{"entity-type":"item","numeric-id":3003228,"id":"Q3003228"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5d969287d02cf50316e6f1cd8d32855d57796c3f","datavalue":{"value":{"amount":"+0.8450314998626709","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":"Q3100204$FFE53283-1FD9-4A53-B445-7A93D5E4EF28","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ff50cbc6eae1f2084c620650aa95944a904e0330","datavalue":{"value":{"entity-type":"item","numeric-id":5464649,"id":"Q5464649"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"08ee7ca155819f41383e47eada414bfb1973ecf2","datavalue":{"value":{"amount":"+0.8017712235450745","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":"Q3100204$B73EB269-B1E8-473C-9FCA-E11D4F31CBD3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2556a49c571b088eb4778b9a55bda1898ff545ef","datavalue":{"value":{"entity-type":"item","numeric-id":3772181,"id":"Q3772181"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c3b6f121bca6b2f428137251fd49c9c7aeb6d053","datavalue":{"value":{"amount":"+0.7800765037536621","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":"Q3100204$C52AAFF1-4730-4923-8C03-41439EB4319E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b311de376cb7ff80a749fd94f0f7c89068deac6d","datavalue":{"value":{"entity-type":"item","numeric-id":5453489,"id":"Q5453489"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d07d5e822e9faf5e5f537c6dcc933fbd4096f111","datavalue":{"value":{"amount":"+0.7716286182403564","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":"Q3100204$4DD5C30C-7E4A-4BBF-AE4C-F7F2C47C00C4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1a68f59ae32b2681c35c7ea8f212502168273b26","datavalue":{"value":{"entity-type":"item","numeric-id":3994509,"id":"Q3994509"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a4fcb199d2f2d49440b16417f1c63d8b4442323d","datavalue":{"value":{"amount":"+0.7686347365379333","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":"Q3100204$7D90B943-53B3-42C8-B2D6-0ED81190B59F","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:3100204","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:3100204"}}}}}