{"entities":{"Q1650410":{"pageid":1661151,"ns":120,"title":"Item:Q1650410","lastrevid":56906331,"modified":"2026-03-24T13:41:55Z","type":"item","id":"Q1650410","labels":{"en":{"language":"en","value":"Implementation of the composition-nominative approach to program formalization in Mizar"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6898239"}},"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":"Q1650410$0DC9519D-1DBD-4459-8D25-9A395E919EAF","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"7afe7903ea5679d840d4e6402e1d41daa7fae58a","datavalue":{"value":{"text":"Implementation of the composition-nominative approach to program formalization in Mizar","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1650410$2ECA3E6D-6DB3-44EA-B0D4-0D8FA1DAE089","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"d7821accf416eb1c13e21ff4d1d90d7a07d496c3","datavalue":{"value":"1390.68183","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1650410$80084779-5F58-4CA9-9EC5-EDC128E57C5D","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"2e5a0a219ac98a153cde5448dff95be1f29ecc27","datavalue":{"value":{"entity-type":"item","numeric-id":271898,"id":"Q271898"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1650410$3759F558-30EC-4AEB-A1EF-690E6DDA9272","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"640c4be06d582c72de984ba8f70a853b3b8bd56b","datavalue":{"value":{"entity-type":"item","numeric-id":271902,"id":"Q271902"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1650410$DCAC1D2E-522F-4527-A80B-061AD35875BD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"5736b10882fcd248ee7728f1c7c88885067ebad5","datavalue":{"value":{"entity-type":"item","numeric-id":271899,"id":"Q271899"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1650410$F4F47BAD-D135-4F47-9CDE-628867FA83FC","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"5e919ee3e1bff25d5819a92667748233ad0caa11","datavalue":{"value":{"entity-type":"item","numeric-id":203304,"id":"Q203304"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1650410$2B7B348C-1060-4600-954B-CD55F9CAABEE","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"f018725447469cf7bbbe6e46592707d7247bbc01","datavalue":{"value":{"time":"+2018-07-03T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1650410$A976800C-4D94-44A7-96EA-80010474F6D8","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"d013e2e9e668f7479f242f1acb30e4ce7ea17f0e","datavalue":{"value":"http://www.math.md/publications/csjm/issues/v26-n1/12569/","type":"string"},"datatype":"url"},"type":"statement","id":"Q1650410$D9CEE0E7-02E4-4B15-98A0-4C789E791ED4","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"5ec63243674f665c4fb8c147a6c6d9e39f607ff1","datavalue":{"value":"68N30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1650410$1CEA3103-1B7D-438D-969F-C23808C8BF37","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"40d293f5d2161e80872b42afb12a3fc45e5d1401","datavalue":{"value":"68Q55","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1650410$21A016A2-00EF-48F8-A701-7F129BC34C32","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1650410$A78D81BF-C3F2-4061-887B-80EA4226247D","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"d0d27a09ab2f46dc6af07fe693678684de245996","datavalue":{"value":"6898239","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1650410$70216FFC-9791-4A9B-95B9-FA705D657856","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f02f4db7bd17ba3fbae1be6bcee13dc9e5aa86bc","datavalue":{"value":"formal methods","type":"string"},"datatype":"string"},"type":"statement","id":"Q1650410$6B63AB42-38B2-4681-AD96-130713886F8B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ae1478f0080b70574ea441c7d2a3b6db779c2f9c","datavalue":{"value":"program semantics","type":"string"},"datatype":"string"},"type":"statement","id":"Q1650410$C3857454-40CF-4F10-89D6-B0A8C5065BF1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e07fc925e4bb734f368e42dee5edd300b93b1714","datavalue":{"value":"semistructured data","type":"string"},"datatype":"string"},"type":"statement","id":"Q1650410$8D136DC3-EB3E-4271-AED3-340F9C9137D2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d5ef51b89dbf72f7181f6b41896d9233a3e6b1ce","datavalue":{"value":"formalization","type":"string"},"datatype":"string"},"type":"statement","id":"Q1650410$3641F0AD-DA13-4CC3-8A95-DC0DDFE72CDF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c6a78675f0dcb3af511ac1d4dfa61901e828bcb8","datavalue":{"value":"proof assistant","type":"string"},"datatype":"string"},"type":"statement","id":"Q1650410$51F5D145-ADCA-47A4-8B6C-29B70CAB1110","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"19c3232540dc15c9350e8393498317de25361cb2","datavalue":{"value":{"entity-type":"item","numeric-id":16873,"id":"Q16873"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1650410$05518F7A-7D03-44B7-9FDA-8C2E1AA84E10","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":"Q1650410$3C431669-D72A-456A-96D3-3250D50FB583","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"6130a72bad290e99b4d30823cf592f64ef05b4a8","datavalue":{"value":{"entity-type":"item","numeric-id":5584402,"id":"Q5584402"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1650410$EB679670-B680-4952-A013-6323E86C2987","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"323dbd6fd6973b3663055cf97da83be885dd9ec7","datavalue":{"value":{"entity-type":"item","numeric-id":5569944,"id":"Q5569944"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1650410$B9E53D52-C66C-4F26-98F2-83DCDA9DB084","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"804d612aa23ca04bde66555843a754f787b9f3b8","datavalue":{"value":{"entity-type":"item","numeric-id":1796766,"id":"Q1796766"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1650410$E6F524E9-EC01-41F8-9D8B-9459F27FA3CD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e3c6d07dd80de4de8f6f1d51aa5d78e790a6fd51","datavalue":{"value":{"entity-type":"item","numeric-id":5812175,"id":"Q5812175"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1650410$3A0BF1CF-2608-45C7-9A47-0BA81B6D4DCB","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a163c60e539c3583acbaf5feb925b9dcb5d12dc0","datavalue":{"value":{"entity-type":"item","numeric-id":5325053,"id":"Q5325053"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"13d357b1d0fe93f733a45b9985107bedc9c39eff","datavalue":{"value":{"amount":"+0.7411090135574341","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":"Q1650410$68F86C46-D721-4EAF-9A2E-BCD501D79DB6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4da69a3e1c1a9becf895f6f0bb027a645b839050","datavalue":{"value":{"entity-type":"item","numeric-id":4628488,"id":"Q4628488"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"09f5aef06ad7368393f39d2264f95f99c3906af0","datavalue":{"value":{"amount":"+0.7330833673477173","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":"Q1650410$6DC4901D-E653-4297-9D39-3DF684FAA1A9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f2e3527c8ff826c8ac797daef0d80602c1118862","datavalue":{"value":{"entity-type":"item","numeric-id":2311522,"id":"Q2311522"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1ea5ce161581bb4f05266ab97539c3756f6b531f","datavalue":{"value":{"amount":"+0.7261391282081604","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":"Q1650410$8D222606-0C3D-4688-961C-099F4DBE1B4F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e6549d517e11201e7e7f703b6dfb328b0122033b","datavalue":{"value":{"entity-type":"item","numeric-id":3183518,"id":"Q3183518"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0f4ac693020a55b2ece88f50ef3cfbd3a81788eb","datavalue":{"value":{"amount":"+0.7257920503616333","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":"Q1650410$B1FE6726-D63C-4D25-98A9-D14BCD1AA43A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6f1e86f454563fb356e0d0a3e6e99b59e950e78b","datavalue":{"value":{"entity-type":"item","numeric-id":1058285,"id":"Q1058285"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c27eab03c2b6eb82252b1145ca58c68ed2c8dc97","datavalue":{"value":{"amount":"+0.7195142507553101","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":"Q1650410$0D0D89D9-1093-4894-B944-482637291A59","rank":"normal"}],"P163":[{"mainsnak":{"snaktype":"value","property":"P163","hash":"601a8be25209c46f574d1c22a38bee2246bce6f6","datavalue":{"value":{"entity-type":"item","numeric-id":57078,"id":"Q57078"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1650410$D5D30226-3FD9-480B-9D18-3D9A9DFA5DC7","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:1650410","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:1650410"}}}}}