{"entities":{"Q1945908":{"pageid":1956650,"ns":120,"title":"Item:Q1945908","lastrevid":69831828,"modified":"2026-04-13T10:38:42Z","type":"item","id":"Q1945908","labels":{"en":{"language":"en","value":"On rewriting rules in Mizar"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6154932"}},"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":"Q1945908$1DD320FA-5D4C-41F5-A6B4-D46CE58B7649","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"cfe90d7cd6ea800e6fd4a980e3f9fe8c40ba66e9","datavalue":{"value":{"text":"On rewriting rules in Mizar","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1945908$58030DA0-A412-489A-AA29-D5D31766FDFF","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"d8b985ff1eb5ea8e2665bc29ba25b44c407359c6","datavalue":{"value":"1260.68376","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1945908$CE2DBE5E-7722-419F-B10C-5A471524F9E5","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"640c4be06d582c72de984ba8f70a853b3b8bd56b","datavalue":{"value":{"entity-type":"item","numeric-id":271902,"id":"Q271902"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1945908$4F32E966-5C3B-4C4F-9E3C-371736DE1983","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":"Q1945908$69777E57-42C3-4D2D-8D5B-20A419FBE06A","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":"Q1945908$F8A61C4E-9D13-435F-A229-AB173B389363","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1945908$7B603907-BCAA-4744-AC16-B041AB8876A9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"6be78f1bad1f2f19058dbde65eb124c0430a7d27","datavalue":{"value":"68W30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1945908$09350D4D-471D-4FA9-B509-AF415F85C942","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"3bb0cb8b5e68b8352258add22f93354e75319841","datavalue":{"value":"6154932","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1945908$72878D29-FFE1-4FCC-9A7A-F6B7828AEA6F","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c6a78675f0dcb3af511ac1d4dfa61901e828bcb8","datavalue":{"value":"proof assistant","type":"string"},"datatype":"string"},"type":"statement","id":"Q1945908$B7756352-E1BB-4BA8-9CFE-7CD0875D81F9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a7245057d33d9a959e820bafe53b372c083536e6","datavalue":{"value":"natural deduction","type":"string"},"datatype":"string"},"type":"statement","id":"Q1945908$670598A8-F215-4AD6-8268-D7165C06E8EF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d17109e875f62271267ba944e1d111a7f52ed69f","datavalue":{"value":"computer algebra system","type":"string"},"datatype":"string"},"type":"statement","id":"Q1945908$E5238E06-A114-4322-9802-6364DD11911A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5a664fc87eb2216b1fad976387dcf6ff589b12b5","datavalue":{"value":"term rewriting","type":"string"},"datatype":"string"},"type":"statement","id":"Q1945908$67D2212A-C34F-4A0C-8E6B-8CFB0D6C37C5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"b0a52f2abcde2ed5d506d011173fb6a54f2d1010","datavalue":{"value":"\\texttt{Mizar}","type":"string"},"datatype":"string"},"type":"statement","id":"Q1945908$70A3C34D-134B-4C48-9AB5-990F736AE63A","rank":"normal"}],"P1463":[{"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":"Q1945908$071ECC27-7AEE-4FB8-923C-5CD30E95BA46","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":"Q1945908$8E67068C-A121-4517-A911-9AD34CFC61A2","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"e8cc9665ae652c9b9cf0583a812b34b78aceb6e8","datavalue":{"value":"https://doi.org/10.1007/s10817-012-9261-6","type":"string"},"datatype":"url"},"type":"statement","id":"Q1945908$B52EAC7C-27DD-4017-843B-D37F6196EF86","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"ab26248ca7001b289a84404aa30d8c78e584600a","datavalue":{"value":"W2042059286","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1945908$5B2E12CE-99A5-4A8A-BF1A-29501D3EC58B","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"819a2535befb2a67f49ee5e43432525215be36de","datavalue":{"value":{"entity-type":"item","numeric-id":4702972,"id":"Q4702972"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1945908$59BB4AD6-D8CA-49E6-8E6E-80EB4FA5EF59","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"65894f2af3b96bcb305bb357ba9e5a69f2e35cbe","datavalue":{"value":{"entity-type":"item","numeric-id":3075243,"id":"Q3075243"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1945908$B15F2E2A-5B0F-446B-8D35-8B9AAA92055C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"826784b29471391d5a5452f2c4d9d6a0b54febd0","datavalue":{"value":{"entity-type":"item","numeric-id":2865746,"id":"Q2865746"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1945908$06FBE739-EE91-4EF2-A217-C9E243FFF732","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ae19a70a8616a64987bb08271f6f085e5255b8c5","datavalue":{"value":{"entity-type":"item","numeric-id":3908476,"id":"Q3908476"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1945908$12D657F1-5C7C-42EC-936E-712B49EE8E94","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":"Q1945908$A566615A-3FEA-4DEB-AF10-6599D8DE7868","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c852981cf03ba0205dbadf36200c00bb56793d8c","datavalue":{"value":{"entity-type":"item","numeric-id":3183518,"id":"Q3183518"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1945908$3FE29B5A-294B-45FD-85C8-8EF288D5677A","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":"Q1945908$07BD77CC-C7B7-44D7-B036-1D3C668253F0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"975126c2667d6964e52988e556bf8223ff836bfd","datavalue":{"value":{"entity-type":"item","numeric-id":3883564,"id":"Q3883564"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1945908$E7D4DC80-F097-4864-B300-3F06ECE9DF59","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c5791c716254aa1932faf4df96272562ac819ae0","datavalue":{"value":{"entity-type":"item","numeric-id":5703869,"id":"Q5703869"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1945908$432B9FAE-261B-4A5B-A6D2-28B7C39118DA","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":"Q1945908$8F5B87FB-4E08-4F13-96AA-840A2DF06392","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7bf17f120be23f1869b8cc6d4b0a9cd5af1d122e","datavalue":{"value":{"entity-type":"item","numeric-id":2767928,"id":"Q2767928"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1945908$871DADE0-10DF-4468-A782-F63D466FA8FA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d09db88e7db8de8a699f35dd014c509760be4233","datavalue":{"value":{"entity-type":"item","numeric-id":4157961,"id":"Q4157961"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1945908$AB23587B-5057-4C8E-B179-C734EBCB0DB0","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"81b72936f4de6b073f87d9f9b72dedb502f7117c","datavalue":{"value":"10.1007/S10817-012-9261-6","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1945908$4BC14FDD-55D5-4ABF-BBD2-7E0288C10277","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e9d46345375cf30c0ce392ba2457e734405cc9d7","datavalue":{"value":{"entity-type":"item","numeric-id":5096184,"id":"Q5096184"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5c3b7c5df0cbc7d2fb2a4f6f4af069e63d4ba8b7","datavalue":{"value":{"amount":"+0.7508116364479065","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":"Q1945908$62B4AC3C-155F-45A2-B6EC-2CCBA4C7A86E","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":"257c035ffa012e280588147abc0a0818e2f6a8c3","datavalue":{"value":{"amount":"+0.7500389814376831","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":"Q1945908$E7FC650D-122B-43FE-B483-503A5B10B014","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"86930e50c98cf354bb283e1562c8ba3467e93c7e","datavalue":{"value":{"entity-type":"item","numeric-id":4413895,"id":"Q4413895"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5eeb6d9e4b23b1214bdb73db0c44b7e56ef20516","datavalue":{"value":{"amount":"+0.7487940788269043","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":"Q1945908$F858391C-6278-49FB-9330-20F77BB7C1EE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8f1c70ed659205385e458fe3a28df7787e8c7705","datavalue":{"value":{"entity-type":"item","numeric-id":3805956,"id":"Q3805956"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"522d4800d32c3320e72ddd15c408a3c2288cde30","datavalue":{"value":{"amount":"+0.7473724484443665","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":"Q1945908$18AA36E3-1343-4470-8509-F5A90979AEF4","rank":"normal"},{"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":"c252af763bd704f3bc02a318e15aa9d78bcf2073","datavalue":{"value":{"amount":"+0.7433374524116516","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":"Q1945908$662174CB-E544-4433-ABDF-328F51945DCD","rank":"normal"}],"P163":[{"mainsnak":{"snaktype":"value","property":"P163","hash":"45fcd4163b5f33e6e8c784f5522d7246c0a1a61e","datavalue":{"value":{"entity-type":"item","numeric-id":57056,"id":"Q57056"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1945908$7DFADC4C-99DF-44F8-AA6D-276A4A7BD9FA","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"On rewriting rules in Mizar","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/On_rewriting_rules_in_Mizar"}}}}}