{"entities":{"Q1945901":{"pageid":1956643,"ns":120,"title":"Item:Q1945901","lastrevid":69831765,"modified":"2026-04-13T10:38:39Z","type":"item","id":"Q1945901","labels":{"en":{"language":"en","value":"Eliciting implicit assumptions of Mizar proofs by property omission"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6154926"}},"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":"Q1945901$89307511-4654-4629-ADB2-40A93E880C12","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"2a50608f3c0f2da9c1240b59d72e566e356a10d8","datavalue":{"value":{"text":"Eliciting implicit assumptions of Mizar proofs by property omission","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1945901$8B8DA8AA-FE48-439A-8B22-AE67426F0E09","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"f5bb71602a8d8b0e59cfdb379918a31d1a6be6ae","datavalue":{"value":"1260.68361","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1945901$CCF712C6-71D6-4DB5-9B13-850EFA7BDA96","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"263b3b42f52ae45efd16753ae3b4c5178f9c0385","datavalue":{"value":{"entity-type":"item","numeric-id":456971,"id":"Q456971"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1945901$DA40F274-5691-487F-9C0F-C0C60AD91765","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":"Q1945901$C5D0E62C-172A-4091-84D1-4D553BA9B33B","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":"Q1945901$60901DC1-14C0-408C-B36D-51DE53C475AC","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"e20d3bfaf4557ec3fb7df93dab4e3d06158214ee","datavalue":{"value":"https://arxiv.org/abs/1109.0633","type":"string"},"datatype":"url"},"type":"statement","id":"Q1945901$C3CB9F1E-BC14-4C4A-B5D7-43722DA979A4","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1945901$75414E5E-5147-4B5F-B58D-D58DF2B2AAF0","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"1168d69ac176023dbf727be0629854563917feb3","datavalue":{"value":"6154926","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1945901$51EA0350-901A-4C1F-B547-8D48FF2329A0","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"21cf102e52d55bb9e3ba4ca1c32b8839281988dc","datavalue":{"value":"interactive theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q1945901$E233E143-FF8D-4955-8247-B4776AB07CCE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"8e79bc83cdd21b11eea8b8bb47ed4c7f694b19e4","datavalue":{"value":"proof dependencies","type":"string"},"datatype":"string"},"type":"statement","id":"Q1945901$B44AD332-CD68-4414-86AC-6F5686B47A13","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"75b42b78dbb6564c3024267b7d2634512fa5c2d9","datavalue":{"value":"proof analysis","type":"string"},"datatype":"string"},"type":"statement","id":"Q1945901$2A0605F5-D93D-4668-B7E3-5C7F8D935B2A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"755fada1e6017ef5ddbb118736ad76ab91e6980c","datavalue":{"value":"large formal libraries","type":"string"},"datatype":"string"},"type":"statement","id":"Q1945901$081E85D5-2CD9-44C6-9F01-844E32591FC5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"55caf05c57404ab910cf1d6d785d791abcc73ea3","datavalue":{"value":"formal proofs","type":"string"},"datatype":"string"},"type":"statement","id":"Q1945901$979E72D9-6A1B-4A69-B7D5-1D90FAADA539","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"b0a52f2abcde2ed5d506d011173fb6a54f2d1010","datavalue":{"value":"\\texttt{Mizar}","type":"string"},"datatype":"string"},"type":"statement","id":"Q1945901$27D5FCBA-FBF4-48CB-8818-D578A1C7E3EA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ddbcb2073b5c7b755f2e5b673e59622629e687d7","datavalue":{"value":"proof assistants","type":"string"},"datatype":"string"},"type":"statement","id":"Q1945901$B529C1D4-DCA8-43DE-86E6-6CBA4EC37A3F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"07b614a858b85b15ce22719eaec7a108ac618711","datavalue":{"value":"implicit assumptions","type":"string"},"datatype":"string"},"type":"statement","id":"Q1945901$C3B0CF3B-AFDE-4A63-A2E7-F156A74772CC","rank":"normal"}],"P1463":[{"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":"Q1945901$FC7CA5EF-D92C-492C-878F-964C58431CDC","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":"Q1945901$306FF636-3992-4B6F-A775-5B7857132216","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"3eaf07f768ca8be71662e20433e73a8eb3a36f15","datavalue":{"value":{"entity-type":"item","numeric-id":21140,"id":"Q21140"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1945901$4A039643-3ABD-465C-8D16-C12C06487450","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"f8ef9006a1bc79ec9ff16a135860884af04d1130","datavalue":{"value":{"entity-type":"item","numeric-id":1333887,"id":"Q1333887"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1945901$A497605D-E000-4CB3-863F-426D543893D3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"cb2a0d26fea35078242c9d2bd845a54b09422961","datavalue":{"value":{"entity-type":"item","numeric-id":17015,"id":"Q17015"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1945901$90849420-8FBA-437B-ADA7-55EFF25D8FCC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"875fd2341d7eaef60a26a549ea0c9adfdf328e2e","datavalue":{"value":{"entity-type":"item","numeric-id":17039,"id":"Q17039"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1945901$939B7C36-2F9B-4DCC-A635-F821C90649C0","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":"Q1945901$78BBA139-1E83-4A56-A2DC-8F886F957951","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":"Q1945901$F39A0807-1D0F-45B2-968F-4B1BFF756EB1","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"b849a2b93642d849691d3658251fc782cf93b3bb","datavalue":{"value":"W3122106493","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1945901$56A948DA-AC58-4A5C-8288-68A28C1F7E40","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"579bdac171075790649277306a9c21fd3b179691","datavalue":{"value":{"entity-type":"item","numeric-id":5200113,"id":"Q5200113"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1945901$3AB460CA-AEA5-4760-BADD-FBD7EC1B53DC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e3c3a2fc034a7c7faa0765e9ae1586daee1601d8","datavalue":{"value":{"entity-type":"item","numeric-id":3096993,"id":"Q3096993"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1945901$B1288E5F-3A82-49B7-9AD9-EA56B550FABD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"494aa31720bff090f87eabeb86ce7380ba058cbf","datavalue":{"value":{"entity-type":"item","numeric-id":5747649,"id":"Q5747649"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1945901$F600F483-9FAC-4C3D-A3A1-61D44F39808E","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":"Q1945901$44243572-032F-4C7C-A003-B12E5BFCB5AE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6946adaf1a8c8f141e0757f8f6f8365e21e858a9","datavalue":{"value":{"entity-type":"item","numeric-id":4099559,"id":"Q4099559"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1945901$55F8A4D3-4872-4626-89C2-D6E580A904D6","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":"Q1945901$F3CE2615-8075-4853-BD4E-E28E9F3D7B14","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"92bd7a7804d462c14eca2f48adcb648eadeff050","datavalue":{"value":{"entity-type":"item","numeric-id":1100932,"id":"Q1100932"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1945901$8A3A6E09-1692-4DF4-B629-50635D9B822C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0430e4a9fe16a78c945c278746cad2959afea463","datavalue":{"value":{"entity-type":"item","numeric-id":3395521,"id":"Q3395521"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1945901$D4C7FCAC-943B-4D04-B9B9-B840F775A25D","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":"Q1945901$B3DC227E-6B85-47E9-984D-7AF997ADC4AF","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":"Q1945901$5CD4BE06-9968-4B8B-83E7-C4508B64E492","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":"Q1945901$63268524-2B64-480B-A90A-731C5776300A","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"d8ea5d5d3c9b69e508b637b9779dc9f0b8f0baae","datavalue":{"value":"10.1007/S10817-012-9264-3","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1945901$7373DEF8-0F78-4B28-AB59-B558DF0EEFAF","rank":"normal"}],"P1643":[{"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":"1b2980f970c5de16caf8614f889f60a903272da6","datavalue":{"value":{"amount":"+0.7033588290214539","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":"Q1945901$C3B67271-D2CE-4470-A977-937041BD99AB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3db6d199add8d33f3d913b30a13b7b56d2fd080f","datavalue":{"value":{"entity-type":"item","numeric-id":5200124,"id":"Q5200124"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c74331f6275ae4f48410d8f8c3f15cc010c5f8c6","datavalue":{"value":{"amount":"+0.691643476486206","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":"Q1945901$FA24CED1-535C-4AE7-A3B9-FBFCAB685174","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e4374daf952f95be8e2d6a4ef5e2444e3d0d7712","datavalue":{"value":{"entity-type":"item","numeric-id":1663215,"id":"Q1663215"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f7674fded8d995abb1435c64dc4c44653047e53b","datavalue":{"value":{"amount":"+0.6863260269165039","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":"Q1945901$A1F06555-CF30-4465-96DF-4A6BBF16BF46","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ca7ff0bff9b3e13356ff885aa48c8da8482419c9","datavalue":{"value":{"entity-type":"item","numeric-id":2817301,"id":"Q2817301"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2584288d158dd5d96db6dcb346c830391d99df07","datavalue":{"value":{"amount":"+0.6828143000602722","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":"Q1945901$02318F63-C013-4DC3-94F2-4DF0E049AE28","rank":"normal"},{"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":"1d7deece9eba80e936f4a8f7258b0737b612fd1d","datavalue":{"value":{"amount":"+0.681556761264801","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":"Q1945901$AD67E895-DF4C-4ED1-BFE7-95BE3BF8F347","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Eliciting implicit assumptions of Mizar proofs by property omission","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Eliciting_implicit_assumptions_of_Mizar_proofs_by_property_omission"}}}}}