{"entities":{"Q2364678":{"pageid":2375421,"ns":120,"title":"Item:Q2364678","lastrevid":52864712,"modified":"2026-01-23T16:23:53Z","type":"item","id":"Q2364678","labels":{"en":{"language":"en","value":"Presentation and manipulation of Mizar properties in an Isabelle object logic"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6751319"}},"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":"Q2364678$9151D681-4D1D-49D8-A3A5-E92D3564734F","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"e9d02a9783b97af2d683dd64fa2d450d7896f89a","datavalue":{"value":{"text":"Presentation and manipulation of Mizar properties in an Isabelle object logic","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2364678$36F63702-F334-40F1-9711-761151A70A38","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"c5941ec8b620636799fdf42ee98d376576849fea","datavalue":{"value":"1367.68250","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2364678$6D0A4AD8-5522-4B6E-A239-9F7D935CFED5","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"b8e09193ef5c67f2accd32bd35c96d949f1f0b6b","datavalue":{"value":"10.1007/978-3-319-62075-6_14","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2364678$AEF5584D-FB3A-4831-89BA-4386CD4FA124","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"6ad6a046b48bbe4ab777309f1d5c19b5fc7dfbda","datavalue":{"value":{"entity-type":"item","numeric-id":286799,"id":"Q286799"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2364678$62BE667E-68D7-453B-807E-0AD6D9975853","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"91705e7e82173950109985f05602a2e2cc8516e0","datavalue":{"value":{"entity-type":"item","numeric-id":286804,"id":"Q286804"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2364678$18C307DF-B17F-40B3-B631-7102253E1DB1","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"36ae9f0663dd67e81623b5f2360b90198adfccf0","datavalue":{"value":{"time":"+2017-07-21T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2364678$B79981AE-C264-43C0-BF72-10F51639B7AB","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"17c833563ed52bc188a660e67b064c854baaeb27","datavalue":{"value":"https://zenodo.org/record/1475065","type":"string"},"datatype":"url"},"type":"statement","id":"Q2364678$B05869E6-6F77-40F9-BB6F-225E05ABFB07","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2364678$06E20C6C-D65D-4A5D-88E3-EFCF7110D0DF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"0c6e71133293256880be082f6af9aa793c57d433","datavalue":{"value":"68T30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2364678$BC398611-DB1B-4424-9CB2-BA5E4966899C","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"4a8cf5b98c0aef54a6b15b11e4f63d043eaa805f","datavalue":{"value":"6751319","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2364678$46F63CD2-9463-4766-9B39-A2E6EC06582D","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"d1ba72d4ceaecc228642fca7b12f0dd0bfed563d","datavalue":{"value":"Q108482130","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2364678$D01BB71F-B864-4536-BE8A-75CC49984F20","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":"Q2364678$4AA4CB80-1F4B-4480-B4BE-C97044FF4FD1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"040fe209bf9959da562393c0e37eb31592733af3","datavalue":{"value":{"entity-type":"item","numeric-id":18957,"id":"Q18957"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2364678$0BA1EF67-56C1-48DE-A402-546F7EC5C49F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"3dcf6ea9ac65c890e0513ced8e4b0dde71e50b0f","datavalue":{"value":{"entity-type":"item","numeric-id":19141,"id":"Q19141"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2364678$F3034D90-0618-4852-A7F0-E2ED27DA98C5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ecb31703c95d92836f5795ab26c09db794aca0b4","datavalue":{"value":{"entity-type":"item","numeric-id":42136,"id":"Q42136"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2364678$0653CB06-F24E-4FE1-B8E3-90153DDE6BF0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"aca41f313ec935c6c7a90dad170b49859b6fac14","datavalue":{"value":{"entity-type":"item","numeric-id":17120,"id":"Q17120"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2364678$F4286C4E-3114-4866-B16D-5EEE4D0DD512","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"550541b08bcfd7113a03dc69a25fcd69cb35ddef","datavalue":{"value":{"entity-type":"item","numeric-id":25224,"id":"Q25224"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2364678$4CEA2668-D3CA-44E5-8D0F-D09980FBD09E","rank":"normal"},{"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":"Q2364678$41025D3C-21C8-47E8-BEC4-C844C7EB0B71","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":"Q2364678$8BCE676A-8369-4D3A-B54E-8592C1C34BE7","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"1b0d721a47173269e91d9e348e213bfa6cff597a","datavalue":{"value":"W2734056180","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2364678$23B18269-5F87-4ED2-BE61-2115472BB43C","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"604f23db2dd4d34a2f60254ad57a8915830982b5","datavalue":{"value":{"entity-type":"item","numeric-id":5200114,"id":"Q5200114"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2364678$30A6EEB9-D5C9-4E87-8D66-2EBA828A720B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"733843eb43f5cdfe85baf6168d9b7e77daeedd24","datavalue":{"value":{"entity-type":"item","numeric-id":4924547,"id":"Q4924547"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2364678$70F39F64-5DC4-47AD-91B2-946FD487E086","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5552c73af9ffa4d08773105bfa675feb6642eb2e","datavalue":{"value":{"entity-type":"item","numeric-id":3453119,"id":"Q3453119"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2364678$9D3768F3-F932-4EBB-9F0A-CD653A0B03DB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d861948f1f6146a05d3ce13e4c51b6e0c074be1f","datavalue":{"value":{"entity-type":"item","numeric-id":286794,"id":"Q286794"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2364678$72F9BBB5-EBDE-40C9-AB68-127881814A1E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e14549321cbae3c57ae9ce6a9266b4af3d64fd4f","datavalue":{"value":{"entity-type":"item","numeric-id":286800,"id":"Q286800"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2364678$F2DDA631-CAC6-4100-B236-66DEA596D5E0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"436d8267b8b601e92bc0ef555ffe6911eece93f5","datavalue":{"value":{"entity-type":"item","numeric-id":1945908,"id":"Q1945908"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2364678$E9F4A6F6-BAD4-4798-90FC-EB3B1073B8F7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"fc5dd7a0147830d02b1314cee235ccefedf59c76","datavalue":{"value":{"entity-type":"item","numeric-id":2817301,"id":"Q2817301"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2364678$EB15B63B-0C35-49B5-8C29-E64D111AE622","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"bde1d1fce6684f6cc1e38b30a0a5bddfab8d8725","datavalue":{"value":{"entity-type":"item","numeric-id":3453108,"id":"Q3453108"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2364678$A3AFAC92-F380-4AB9-B7D3-C610112E1755","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0136d3bc330af377385e6266bfd9e4c2d4c7a96c","datavalue":{"value":{"entity-type":"item","numeric-id":1319386,"id":"Q1319386"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2364678$98F5408D-970A-405D-809C-9BF389BEFAD4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"631fb0653addd3bb7a28e2d83e1cdbb5e8b075b5","datavalue":{"value":{"entity-type":"item","numeric-id":286805,"id":"Q286805"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2364678$2127909C-6DCE-4A1B-9B4D-19573F085FB2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"90a8e71b34c70e726e0c295f8b429b043df8614e","datavalue":{"value":{"entity-type":"item","numeric-id":5400853,"id":"Q5400853"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2364678$5C21A1EC-CE6A-4C67-A47B-149559536935","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ec8995610696de6f75b854cd93b7ba9a971f10e6","datavalue":{"value":{"entity-type":"item","numeric-id":3183521,"id":"Q3183521"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2364678$63CA3CC8-6216-4F62-9A5E-27D65107B3F8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3c6f2b5700f03be5d761a1df5375a7e275478f2c","datavalue":{"value":{"entity-type":"item","numeric-id":841684,"id":"Q841684"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2364678$F30AB791-FE33-4E9D-8C77-B2390FD423BB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"81087b834bd0f0342fd52d99726619dd5c97caec","datavalue":{"value":{"entity-type":"item","numeric-id":3543647,"id":"Q3543647"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2364678$DBFBD01A-3A06-44AE-BCAA-6B3F5C6DE32A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"aa501f8d67d6302c19c53708c34f273d7a39ff38","datavalue":{"value":{"entity-type":"item","numeric-id":819987,"id":"Q819987"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2364678$D9722A55-F33C-4F08-8944-44E41EEE7522","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4e9a18d2fa29298c78dc202aae96a37069cc785a","datavalue":{"value":{"entity-type":"item","numeric-id":2323445,"id":"Q2323445"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4c6ce22e8e158e8532f7876771a65b38b2df78d6","datavalue":{"value":{"amount":"+0.8296056985855103","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":"Q2364678$A341B860-AD07-4E73-B60D-B1AA2F0E8ABE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c1fbe8f76631e9b24e2621b72c3ad8cc01fc1fd0","datavalue":{"value":{"entity-type":"item","numeric-id":1868515,"id":"Q1868515"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"93107f0a594df24ae69cd6ab89d1d58db5176f2a","datavalue":{"value":{"amount":"+0.7584801316261292","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":"Q2364678$4759A794-D21F-4CA0-B127-8A6682F97A79","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ef914c5d16ae991870856bd539a5283395a477b7","datavalue":{"value":{"entity-type":"item","numeric-id":3543647,"id":"Q3543647"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"68a8d8ce85ea8e95a9455a05c6de749bbb26709d","datavalue":{"value":{"amount":"+0.755439817905426","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":"Q2364678$7D2B31C0-BFE7-4D1D-B237-8064B5736F29","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"eee2626a7ebeafe9534d0338c5aeb25841f2e563","datavalue":{"value":{"entity-type":"item","numeric-id":2867936,"id":"Q2867936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"22582f053031bba0975e193e6c28c0a106a9e0ce","datavalue":{"value":{"amount":"+0.7522937059402466","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":"Q2364678$FAEF42BF-8A4D-4305-B694-CBE8E7459584","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f3127bb4bb85b3d61c1c9048202e7949263aa206","datavalue":{"value":{"entity-type":"item","numeric-id":1798961,"id":"Q1798961"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b57573c995434a554e4c34d8d10ed44a7653f85f","datavalue":{"value":{"amount":"+0.7501062750816345","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":"Q2364678$74DB08FF-C4EA-4268-9A40-3999AC3E716B","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:2364678","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:2364678"}}}}}