{"entities":{"Q877826":{"pageid":879674,"ns":120,"title":"Item:Q877826","lastrevid":65062608,"modified":"2026-04-12T00:03:57Z","type":"item","id":"Q877826","labels":{"en":{"language":"en","value":"MPTP 0.2: Design, implementation, and initial experiments"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5149170"}},"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":"Q877826$FF44B9D0-ABE5-4D24-9E44-2AA9B086BD7C","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"50592b27d86129cf406a60f068e43969fe3dd0cc","datavalue":{"value":{"text":"MPTP 0.2: Design, implementation, and initial experiments","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q877826$3DF47FFA-A402-42F7-8D30-7656E7C668CD","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"9d9917b1e48a5e03184764f5e79fac757d54ea0f","datavalue":{"value":"1113.68095","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q877826$D771FEBE-69DA-4E16-BDC1-E8B3E0152201","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":"Q877826$F85A1D47-CD79-4E60-8C93-E0E00EEB8AEF","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":"Q877826$F4CB7EEE-0EB9-4AC2-B9E4-C53BFB8085BE","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"705732f6c443403985df27568b16305b8e45450f","datavalue":{"value":{"time":"+2007-05-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":"Q877826$55272CCA-6735-4B4F-A0E7-D8C86D36860E","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q877826$77B91AB2-B67F-49D9-AC04-3AA93810E724","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"d3f4a1d6e5b7f329f6ac6621bad29346a0b86b97","datavalue":{"value":"5149170","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q877826$8EE54E3F-5DE8-4AC7-BEC9-BDBD5F455116","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4050193275c80324b0fbbd6b500fb6b0d266f8fc","datavalue":{"value":"Mizar Problems for Theorem Proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q877826$553590F5-6968-41D8-BD08-D4F912266453","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"b443b776731e3bc75eb79b752e7ef8c4cee2d97a","datavalue":{"value":{"entity-type":"item","numeric-id":15455,"id":"Q15455"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q877826$DA05895E-E8AB-49C7-8256-24DF10535709","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":"Q877826$C2368C46-D896-43D7-9E5E-41BB6D09FDC8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"effe99d4b547ffcbc07915d8ced5dc197768f166","datavalue":{"value":{"entity-type":"item","numeric-id":15028,"id":"Q15028"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q877826$B7305C6F-FE90-4CD2-BAD1-4C77C860CD70","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"7cccd35b34888307d4ad7b137783609eb5c56b79","datavalue":{"value":{"entity-type":"item","numeric-id":16825,"id":"Q16825"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q877826$6CF13A7A-5AD3-4262-9129-68684BA4988B","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":"Q877826$860B79C7-FF64-41BA-95E1-7124DB6F6950","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":"Q877826$95DBA641-06B8-4152-8A47-49DEC1FB6DB2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"d3ed9701b24c07e8ddeb19932e1fa77191c06e95","datavalue":{"value":{"entity-type":"item","numeric-id":16327,"id":"Q16327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q877826$86F4A5CE-637F-4956-9A32-2BB56BBA76E8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"1017108dce3983431546a14c274f65bc4aaae70b","datavalue":{"value":{"entity-type":"item","numeric-id":22154,"id":"Q22154"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q877826$3472867C-19B7-4A9B-B1C5-96A7413970A9","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":"Q877826$72E9E150-0CCA-4384-86A1-15252A0BE25C","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"abf41e427ac246f53bf285670e20bfe796e6bcbc","datavalue":{"value":"https://doi.org/10.1007/s10817-006-9032-3","type":"string"},"datatype":"url"},"type":"statement","id":"Q877826$A9FD56FC-AF9C-4DF7-A48F-6788172453D3","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"38f0962363641c0d1b9b6be2a4e0294b66615899","datavalue":{"value":"W1995539874","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q877826$46656906-97DE-4067-90D9-3232ABC8B2B3","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"3db96d49cd835a72b0287fd80a8a1bd9f27d72c8","datavalue":{"value":{"entity-type":"item","numeric-id":704809,"id":"Q704809"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q877826$19CFBF42-3F86-445E-A432-0B39406C3211","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3c96b723515f39843f3d28d31678b33cd7d51ac3","datavalue":{"value":{"entity-type":"item","numeric-id":5313076,"id":"Q5313076"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q877826$E31A41D4-01A5-422E-9D44-923BC9DF6FDE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"307c4cd3464c8600dbbfd076f79f5381061b8199","datavalue":{"value":{"entity-type":"item","numeric-id":4413887,"id":"Q4413887"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q877826$8657AB8E-C2BD-4A62-9722-72FCA9F809DB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0e4028b0215dcfb37982ffb4f5fd7958ff82b3a7","datavalue":{"value":{"entity-type":"item","numeric-id":5313077,"id":"Q5313077"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q877826$92FDF3D2-2581-4B3C-BF55-38D7116A0E84","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"359ad93afb2d52ec5ce475aa0a446e7fc3208f47","datavalue":{"value":{"entity-type":"item","numeric-id":4503907,"id":"Q4503907"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q877826$5983DB3A-36E6-4CB6-8404-F95DCCB3687D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7a5ff25f5fdb6aa0631467e77b27102f490b4f3f","datavalue":{"value":{"entity-type":"item","numeric-id":5900726,"id":"Q5900726"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q877826$8B148B28-5CD3-4DD6-9782-EA6E9C2BFCAB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3239d3bc022112b37f4da6991a3c7bf09667ee35","datavalue":{"value":{"entity-type":"item","numeric-id":1196302,"id":"Q1196302"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q877826$4D0D59C6-DD5C-4357-8FBB-5AC194B9278F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c52cd1a25a23d6ee1d2d790b85193089c176c154","datavalue":{"value":{"entity-type":"item","numeric-id":1840387,"id":"Q1840387"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q877826$5297A4B2-04A0-432F-8ACC-D91966ED42ED","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ec41d91b97fe450aba006d86ee1b6e337fcab2ff","datavalue":{"value":{"entity-type":"item","numeric-id":5313068,"id":"Q5313068"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q877826$E8328534-EA5B-4C70-8C99-571137AD1A4C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ac9daa4057ed7a04c427228a37f513d691eccddc","datavalue":{"value":{"entity-type":"item","numeric-id":2757973,"id":"Q2757973"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q877826$33E41125-500C-4B62-96EE-C5A6EBEDD6D2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0cb051a6b1eb9b88364c46513701492fc0e99189","datavalue":{"value":{"entity-type":"item","numeric-id":3150300,"id":"Q3150300"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q877826$FF4D2B26-12DE-4502-AACA-2F86750A618B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c18eae0d93c62338c42d5358a66e2303bf3601de","datavalue":{"value":{"entity-type":"item","numeric-id":1961913,"id":"Q1961913"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q877826$F650D881-F77A-480D-BB82-C184A157D200","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"93fc8985b7898988b7d52edb5c0cd61c1b917df6","datavalue":{"value":{"entity-type":"item","numeric-id":3150301,"id":"Q3150301"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q877826$CCE45D36-8549-4E3C-ACB2-5BB1AE1193BA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2c5b09e879fc9e6d166a18cb26ec583e2bf401aa","datavalue":{"value":{"entity-type":"item","numeric-id":1272614,"id":"Q1272614"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q877826$CBD8EB36-3743-49AF-B253-9C0041A514D0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"fbe0bfb57e9a97e56fde1afbd62d0dd2171c33df","datavalue":{"value":{"entity-type":"item","numeric-id":4413895,"id":"Q4413895"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q877826$5E7A558D-D7F4-45DA-A121-89A3C1A99CA1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6dbaa83286082fe9f22efc1424c5503085916666","datavalue":{"value":{"entity-type":"item","numeric-id":556682,"id":"Q556682"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q877826$0E03F93F-839C-4236-B521-0655A9EE7DD9","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":"Q877826$088BB259-F05F-41BB-8C24-51F9549D7E3C","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":"Q877826$5D565594-2886-4587-96B2-42BE29D382D5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0e5fdc7a388e99bd2ab8aeeef9f0d0e53fac4618","datavalue":{"value":{"entity-type":"item","numeric-id":4413894,"id":"Q4413894"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q877826$D350E082-60D1-45C8-979C-56F56B1349A8","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"091f40114f69d607c27c1925fd4c793311e77364","datavalue":{"value":"10.1007/S10817-006-9032-3","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q877826$136007D4-C591-4BEB-92E9-CFE95D70C908","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3b168262f9e1b4514313a24dfabf8223d2ad31a3","datavalue":{"value":{"entity-type":"item","numeric-id":556682,"id":"Q556682"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e04ce99201f55a5408a63ffd97109fa18ab25033","datavalue":{"value":{"amount":"+0.9313353896141052","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":"Q877826$106A2331-99B0-4E14-867E-0CFF3ED33E3F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"833679bd5dba8272dd461558b8d437f3c0e999af","datavalue":{"value":{"entity-type":"item","numeric-id":4916228,"id":"Q4916228"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6ad9ed33e227d0ddb4ecf3a7f46cb0d76ed84f80","datavalue":{"value":{"amount":"+0.9218416810035706","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":"Q877826$7DA8F828-9C8A-409B-AB54-C3EB1390008C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"13f103237e1b4889a22b078c6687a2ac0c70875b","datavalue":{"value":{"entity-type":"item","numeric-id":5210777,"id":"Q5210777"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"da4fbae6f622d760c4b8552b2f942a32a0bc3270","datavalue":{"value":{"amount":"+0.8169652819633484","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":"Q877826$CF4DD95D-59BB-4F87-B204-04492FCC43EF","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":"fd3d6b06afc8d7a9beeee8dbea303f5dfe0b6d09","datavalue":{"value":{"amount":"+0.8126447200775146","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":"Q877826$55C6AADA-3430-4D72-A4D5-9757FA78B358","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":"70bf343b7dfeef8c75548065f38e3e83619f8110","datavalue":{"value":{"amount":"+0.8115426898002625","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":"Q877826$2F475131-AA00-459E-ABCB-97821EAB7F37","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"MPTP 0.2: Design, implementation, and initial experiments","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/MPTP_0.2:_Design,_implementation,_and_initial_experiments"}}}}}