{"entities":{"Q1945905":{"pageid":1956647,"ns":120,"title":"Item:Q1945905","lastrevid":69831801,"modified":"2026-04-13T10:38:40Z","type":"item","id":"Q1945905","labels":{"en":{"language":"en","value":"ATP and presentation service for Mizar formalizations"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6154930"}},"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":"Q1945905$9F98753C-89EA-45BA-BD2F-08F0CD70C8D5","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"c02bb2d814ef059cc5487202b4dce54a8121c243","datavalue":{"value":{"text":"ATP and presentation service for Mizar formalizations","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1945905$1263405E-7DE7-4958-8436-7CB3EAD83A77","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"dbc76ddc732a43c323ab15a6bad9c81969633b44","datavalue":{"value":"1260.68380","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1945905$03FB847D-304A-4B5F-8881-4F7B27155CB3","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"dc204e2e78d924e815f2b640ec35c8c2356ad41f","datavalue":{"value":{"entity-type":"item","numeric-id":286786,"id":"Q286786"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1945905$FE987046-E426-4CF3-B7B0-91644C58A883","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"9d72ee9ffde9510a13b5bea91934f187bdc57c7e","datavalue":{"value":{"entity-type":"item","numeric-id":467775,"id":"Q467775"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1945905$BF1FC026-27B2-46EA-AE45-161FB7C3645D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"6c6d707c999cc6d62a42a2f34c4e05c6ede74383","datavalue":{"value":{"entity-type":"item","numeric-id":679254,"id":"Q679254"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1945905$546228AD-EEA4-41A1-9F05-6F6F198FAE88","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"b84cc8b5923f45dc86ae69f67f68bf56d7ecfce9","datavalue":{"value":{"entity-type":"item","numeric-id":174771,"id":"Q174771"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1945905$3481C3C5-3BB5-4FC0-848B-6C87BFE743E5","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"4bad757aec17a8570e2102d57df4c93baefd6019","datavalue":{"value":{"time":"+2013-04-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":"Q1945905$6BAE0FBD-0BBC-4FC5-95AC-C93E4F401107","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"b50f24128836dd8a727890439a1509fb1b058b15","datavalue":{"value":"https://arxiv.org/abs/1109.0616","type":"string"},"datatype":"url"},"type":"statement","id":"Q1945905$75C4D37F-2B17-46D0-B0C1-BE3762D388DD","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1945905$CC2FCC66-C751-4770-AAB7-4C83ECC75DD7","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"f563c702f824af84bb4d8cafd65d3b61a5847003","datavalue":{"value":"6154930","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1945905$BE69D082-4136-4B2C-93B4-5535C50BAC2C","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1ca1042868ff4f694776e4b2c62ec66638c4ef91","datavalue":{"value":"automated reasoning","type":"string"},"datatype":"string"},"type":"statement","id":"Q1945905$9031CD54-182B-4BB9-ABAA-D3659D2D22C1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"b0a52f2abcde2ed5d506d011173fb6a54f2d1010","datavalue":{"value":"\\texttt{Mizar}","type":"string"},"datatype":"string"},"type":"statement","id":"Q1945905$CA0E8706-E8CC-4E83-9108-A7075530BC61","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"21cf102e52d55bb9e3ba4ca1c32b8839281988dc","datavalue":{"value":"interactive theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q1945905$0B7BF5AC-E889-4E39-B425-CDECA63ED509","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d5f15d27f8faddc16578e6e462aa89cf3f8d4036","datavalue":{"value":"automated reasoning in large theories","type":"string"},"datatype":"string"},"type":"statement","id":"Q1945905$AC72D3D5-2936-43BA-AA5A-D4E9AAC36571","rank":"normal"}],"P1463":[{"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":"Q1945905$06A57F2A-318D-4CA5-9DE7-F51D55A4DDD1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"484f589bd857c6ecd5604196ba88033adb11a795","datavalue":{"value":{"entity-type":"item","numeric-id":15128,"id":"Q15128"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1945905$6C7779B3-DC72-464E-929D-3F889532AD06","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":"Q1945905$0BAE04C5-2ED6-4D18-AB75-A536A081C0E4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"9b0860d94af5fdff4b5635709ae334aacdf07ca1","datavalue":{"value":{"entity-type":"item","numeric-id":19106,"id":"Q19106"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1945905$87714A85-1C65-4F4F-B611-8914BE3EE287","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"05ea0f807e9dc1229f0a5e44480e85f8c5ae2877","datavalue":{"value":{"entity-type":"item","numeric-id":14521,"id":"Q14521"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1945905$D16E3A72-B0CF-4C2D-94A3-878883211A72","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"62af2c5e450adf37bd9acb47c5a55b60b68447ea","datavalue":{"value":{"entity-type":"item","numeric-id":22241,"id":"Q22241"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1945905$EC92CB4F-2334-4F4D-8485-C84539741EBD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"133e2e5701b3435e4a72bb2a6345ff9894f7c6da","datavalue":{"value":{"entity-type":"item","numeric-id":22369,"id":"Q22369"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1945905$F068505A-B5DC-4A71-8DBF-D11F94E06967","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"31d2ddeef485fccfd3a5fe32ea329d2b65b4f1b4","datavalue":{"value":{"entity-type":"item","numeric-id":35396,"id":"Q35396"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1945905$D068FBA9-091B-4D7B-A7B6-6E8477240C07","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"9c2ac6c1c15bd263207487c53115a7cc6abe2547","datavalue":{"value":{"entity-type":"item","numeric-id":19033,"id":"Q19033"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1945905$DD9E38E2-B8B3-4964-81B7-A6775BD7865B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"19db008058ce3a679389c190541b4b00e350555f","datavalue":{"value":{"entity-type":"item","numeric-id":27113,"id":"Q27113"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1945905$A92F46F7-A09B-4624-BF98-5E7E6C697CF7","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":"Q1945905$793B2DA2-3242-4A13-B97F-F2A0D7E588C9","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"4d86536ab6b1a8280ee947f315a58faa81d045a1","datavalue":{"value":"W2399753239","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1945905$1671D9BE-DA29-469C-9E81-C9A37E06982E","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"29b0802dd9ffb89108bee25aa26120dffc46ad60","datavalue":{"value":{"entity-type":"item","numeric-id":2352489,"id":"Q2352489"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1945905$9A0D8A96-F8E8-4AE8-8660-4D986D8E2F2C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"eb1bab11b75e766c233c3a1b9a3682b90b0e288d","datavalue":{"value":{"entity-type":"item","numeric-id":3075247,"id":"Q3075247"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1945905$59A700E0-3852-48C7-AC0B-56B47DE22ED3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4fac8018d67440c6289d41ba6a99a91f9d3e2025","datavalue":{"value":{"entity-type":"item","numeric-id":2494223,"id":"Q2494223"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1945905$0466A600-EA09-46A0-BF2B-65D08310A601","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6c50bf30b5dabdf4dda50dde9e43de872f1c8761","datavalue":{"value":{"entity-type":"item","numeric-id":5200032,"id":"Q5200032"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1945905$68C91252-C487-42BC-A4A7-B5AB26E6B401","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"741b1c2a1697c669d1b3bbdff87dd79f9f007366","datavalue":{"value":{"entity-type":"item","numeric-id":1006731,"id":"Q1006731"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1945905$F3A2B283-96A3-4D47-9FF3-C04BA317B2A1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8dc8e3a70353874ae71b2b5e055e522ed5b6378c","datavalue":{"value":{"entity-type":"item","numeric-id":5847741,"id":"Q5847741"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1945905$133193D1-A37D-4EBC-A562-357F86CA08C1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"78674dd617192aae3b1bc06dfc8223a2e686c21f","datavalue":{"value":{"entity-type":"item","numeric-id":2852152,"id":"Q2852152"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1945905$F093553E-1E5E-42D4-AF51-F829F8598875","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ae2da92fb913582a601af7173c06716220bbf7eb","datavalue":{"value":{"entity-type":"item","numeric-id":5898530,"id":"Q5898530"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1945905$995126AB-0D35-4760-93E9-3D926BB0AC5B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b514a4f7338b45fdf5de5487918e2ae3d624f2f1","datavalue":{"value":{"entity-type":"item","numeric-id":865631,"id":"Q865631"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1945905$EF7D7235-28B4-485A-9C89-52F578447451","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"bbf7b4ce3ab96d4236a4c36e2f89589530011a89","datavalue":{"value":{"entity-type":"item","numeric-id":877826,"id":"Q877826"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1945905$461447FA-BE52-401D-846F-5C691DCE436C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a1d0235461a49d24f36b9a64ea22f473f8531ad7","datavalue":{"value":{"entity-type":"item","numeric-id":3582731,"id":"Q3582731"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1945905$29CF9760-B11D-4617-AD39-E0549B462FFD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"fe1b7572751e7c38d04d8597a88021abb417e889","datavalue":{"value":{"entity-type":"item","numeric-id":5747877,"id":"Q5747877"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1945905$04AC9C85-78C8-4278-9B25-5F80E71D31DA","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":"Q1945905$83D8F773-DCD5-49EF-8EE2-9F1372289E15","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9655c068a195af6d54bbb62184581b058670a2b2","datavalue":{"value":{"entity-type":"item","numeric-id":3541722,"id":"Q3541722"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1945905$927EB625-4BB6-474E-BFE3-F34F2D001A05","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1e1a8094411c4c770dd370a45c2db874b8897938","datavalue":{"value":{"entity-type":"item","numeric-id":3066112,"id":"Q3066112"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1945905$6A8B5D1E-CB05-404B-98A8-3CFEDF6200B8","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"b11ffe861ff3acd9ac3b7826bf6a327c420a004b","datavalue":{"value":"10.1007/S10817-012-9269-Y","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1945905$84D8BEFE-5E9A-4793-B8F7-F689DDBAA848","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e0a3e291f1f17745f7efdf0798b5008ce6b5f5c7","datavalue":{"value":{"entity-type":"item","numeric-id":3582702,"id":"Q3582702"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"aa2dbf2c6d012cf62b7a6955001465aa01c50e68","datavalue":{"value":{"amount":"+0.8662517070770264","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":"Q1945905$71C5A1C7-21EC-4AA1-A3F2-3BBEDFD08A9D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2f3833b6921aee56ef7759acb6d3f6c8713ccb4d","datavalue":{"value":{"entity-type":"item","numeric-id":286800,"id":"Q286800"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c8b21e9e6c994db0d32ea74ba9e21ebece1ab721","datavalue":{"value":{"amount":"+0.8435969352722168","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":"Q1945905$6828E8BD-19FA-4782-94E5-B99D2B5C9E91","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d864bf8a230add6bdc1dd6fe6bd222a019572354","datavalue":{"value":{"entity-type":"item","numeric-id":841684,"id":"Q841684"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a3d489c27d33ed3e85da086dc493817a77945d96","datavalue":{"value":{"amount":"+0.8198281526565552","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":"Q1945905$E558C400-6AFE-4E3A-8DB4-DB0E1D1CBB6A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c6b4440e24c330497025549da4d4dc8ba9f23acd","datavalue":{"value":{"entity-type":"item","numeric-id":5747877,"id":"Q5747877"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1d362194180498c646384b4699f2d40bd7543543","datavalue":{"value":{"amount":"+0.8123860359191895","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":"Q1945905$6D8A96C4-A6B1-4BE0-BF6A-155FB5465F69","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"63c88c73eb0f33863fc007467a9962367e1e0911","datavalue":{"value":{"entity-type":"item","numeric-id":877826,"id":"Q877826"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"98cc9e66bba43a3cf9c2cdb211560b02b80c2ee2","datavalue":{"value":{"amount":"+0.8067488074302673","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":"Q1945905$C8065E6F-03B0-4748-B387-D083B6CEF64F","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"ATP and presentation service for Mizar formalizations","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/ATP_and_presentation_service_for_Mizar_formalizations"}}}}}