{"entities":{"Q865631":{"pageid":867479,"ns":120,"title":"Item:Q865631","lastrevid":64941783,"modified":"2026-04-11T23:15:10Z","type":"item","id":"Q865631","labels":{"en":{"language":"en","value":"MizarMode -- an integrated proof assistance tool for the Mizar way of formalizing mathematics"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5128346"}},"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":"Q865631$D30BE26A-045D-46E2-8777-A389F095988B","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"0404eaf1e50dc75340c60fc264894b32a372f305","datavalue":{"value":{"text":"MizarMode -- an integrated proof assistance tool for the Mizar way of formalizing mathematics","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q865631$6893D6EE-43FA-47DD-A180-B970192984C4","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"0031d0cbd3481a37f876a6667f37c68248106f33","datavalue":{"value":"1107.68103","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q865631$4148A027-9CE0-43D2-A4FE-EC615546A002","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":"Q865631$785BB19F-FB88-4867-B7BC-43B10E05C535","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"fd9c858b64e538228c66f00c768fd1506ee71010","datavalue":{"value":{"entity-type":"item","numeric-id":124852,"id":"Q124852"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q865631$64F15182-C091-4BC1-A82A-562048D6534F","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"b6a3b01ed43848088ad19bc3cf2f29651a0e98f7","datavalue":{"value":{"time":"+2007-02-20T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q865631$75BC48DB-2A01-4202-9892-EC9AE1597F72","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q865631$2E94FD0A-1BF1-4C6C-A15A-AD3A6B82ED47","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"a200c3f3a760867e37900ce30a8bbd260257497b","datavalue":{"value":"5128346","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q865631$88261EEC-490A-4D43-83E6-8F01A9F2C406","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"571c0e1fb7a78a4a545c4f12cd6536c1efe33bd7","datavalue":{"value":"Mizar","type":"string"},"datatype":"string"},"type":"statement","id":"Q865631$39407155-2A46-48B1-BBF8-9CF8880ACCD8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"52484de527213600564e61411b21b87251ace8d3","datavalue":{"value":"MizarMode","type":"string"},"datatype":"string"},"type":"statement","id":"Q865631$643F1D67-09A9-40E0-A4DE-7734FE88FEB5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"6488672f8085da4e90899ca4308539c7c2c35609","datavalue":{"value":"proof assistance","type":"string"},"datatype":"string"},"type":"statement","id":"Q865631$19D35958-48EB-4325-BA35-A457587768C5","rank":"normal"}],"P1463":[{"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":"Q865631$B19BBF7A-258B-45BD-83DA-DF95E323D7E3","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":"Q865631$C9A37DC6-B830-4A33-8BF2-01C8F64F6590","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":"Q865631$0DE2FC8C-BAE6-4FE5-84EA-66E50E095F4E","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":"Q865631$BC08D5D0-DC6A-4405-B404-06159EEC1E20","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":"Q865631$0E6CB1E1-BD55-4AD0-B3A5-C6F5F28894AA","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":"Q865631$C23B514E-85B2-414B-8549-FDB4E657E358","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"1ae5656a5761b312d2c8a5d729c60a5261b2afc7","datavalue":{"value":"https://doi.org/10.1016/j.jal.2005.10.004","type":"string"},"datatype":"url"},"type":"statement","id":"Q865631$DB8D702F-9DAB-4E1E-AB4B-4EB912CE39C2","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"9e728cfc054ca2958e3a013c300ad636832ae32c","datavalue":{"value":"W1972647229","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q865631$158DA0A5-5665-43C2-832D-340819D59DB4","rank":"normal"}],"P223":[{"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":"Q865631$682B1D52-C210-4889-96E4-4F2681E7C265","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":"Q865631$D13DDA2E-6ED0-4A28-9587-AF86AB2EE4DD","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":"Q865631$3E82539E-0C90-46A5-AACE-DE58A9E15655","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":"Q865631$DBD70717-765C-45B1-B923-555ED86B7829","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":"Q865631$BC548B7C-BC71-4EA6-AAFF-0ECFEDB86573","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":"Q865631$D8375F25-FEFE-4332-8D8B-2321D72C2601","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"8981666710885996f99e7c212051915ca7880fe0","datavalue":{"value":"10.1016/J.JAL.2005.10.004","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q865631$987246A3-E3AB-4257-97EC-1B68D5C236EF","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3ed25aa4185f2e815bad791afac995de061e6cde","datavalue":{"value":{"entity-type":"item","numeric-id":3453119,"id":"Q3453119"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"07181f8f7c23f38ba41c20e2fd105955edbad2a4","datavalue":{"value":{"amount":"+0.8343917727470398","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":"Q865631$DB6D8AF7-B497-48C6-8371-4C1C073DABAF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0836461b86e5f3f9b2683c3a2c12fce3a6959131","datavalue":{"value":{"entity-type":"item","numeric-id":4664918,"id":"Q4664918"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"879775e3809e54137df91fe54b0c3524a0229dce","datavalue":{"value":{"amount":"+0.807415783405304","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":"Q865631$2848ECFF-B201-4AD5-8EEB-381959255196","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"056bd3306219ab81399e7d152a9e6f1d7dd0aa1b","datavalue":{"value":{"entity-type":"item","numeric-id":1945910,"id":"Q1945910"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ab3209605ed88b8f93d1a0af03e4dfdf37caf2f1","datavalue":{"value":{"amount":"+0.7978703379631042","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":"Q865631$47E1BBE8-6A0B-4835-AF31-90969FA9118A","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":"ddc6e85dc4b52859210e62945d722630e2bc2258","datavalue":{"value":{"amount":"+0.7947878837585449","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":"Q865631$FEB48B30-8770-45A4-9063-4DCFCE4C7D9E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"efe65b0ff0f46d73c021ccb0e441e1cae6f5647a","datavalue":{"value":{"entity-type":"item","numeric-id":5313077,"id":"Q5313077"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a531d379a09d4e0d86000992ef7bdd63a0559513","datavalue":{"value":{"amount":"+0.794520378112793","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":"Q865631$7980E324-CBEE-469D-9989-F1E511E56B03","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"MizarMode -- an integrated proof assistance tool for the Mizar way of formalizing mathematics","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/MizarMode_--_an_integrated_proof_assistance_tool_for_the_Mizar_way_of_formalizing_mathematics"}}}}}