{"entities":{"Q5495936":{"pageid":7525496,"ns":120,"title":"Item:Q5495936","lastrevid":41262288,"modified":"2025-04-26T03:10:27Z","type":"item","id":"Q5495936","labels":{"en":{"language":"en","value":"Automated Improving of Proof Legibility in the Mizar System"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6327274"}},"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":"Q5495936$976AFFD2-0E8E-4A05-A4EE-614E5B7F29D0","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"f020aa03e4d433b3d44b92332331c41800ce9a02","datavalue":{"value":{"text":"Automated Improving of Proof Legibility in the Mizar System","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5495936$9FC3F605-D5A0-41D8-87C8-70DF2CA87E13","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"df5f170b2c63e7f2647c749068e394b6fac6c9a3","datavalue":{"value":"1304.68160","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5495936$7456C13F-CF2E-4BC0-95C8-292825EAC217","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"2bc1fbaa2b557fe63bebdcad7eabb6fc9c2aba0c","datavalue":{"value":"10.1007/978-3-319-08434-3_27","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5495936$3F4FD763-D753-4186-8C13-3E00043C7A84","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"91705e7e82173950109985f05602a2e2cc8516e0","datavalue":{"value":{"entity-type":"item","numeric-id":286804,"id":"Q286804"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5495936$6FAB7E46-48F2-4617-B188-67909DC5F0F6","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"85c07c7737819bff773f78e2590a3bb761fe677b","datavalue":{"value":{"entity-type":"item","numeric-id":162374,"id":"Q162374"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5495936$C5CC8727-DA1B-4092-B4A3-F98F5688838C","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"1c94d745affbb1f035e3911adf053858df897bb7","datavalue":{"value":{"time":"+2014-08-07T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5495936$40A8199B-FB06-4261-9D6A-2FFF04BAFCF9","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5495936$FF65A9DB-3CC4-4AF4-83E7-3DAF08D5E0B7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"0c6e71133293256880be082f6af9aa793c57d433","datavalue":{"value":"68T30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5495936$C435CC61-50F0-4638-A052-339A2ECEE696","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"3d738cfa2bab4b5109efaad12a8c6f359305b337","datavalue":{"value":"6327274","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5495936$B49E7119-A504-4607-9A61-4E0B79D8ECDE","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ba2c052f5a4899771a06589f4b67761feab9f86e","datavalue":{"value":"operations on languages","type":"string"},"datatype":"string"},"type":"statement","id":"Q5495936$AB02D726-AD54-4454-90B0-E604FA6A7B63","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"b9a014fb352330ff30aef34ca8515ef7c4b7a61d","datavalue":{"value":"legibility of proofs","type":"string"},"datatype":"string"},"type":"statement","id":"Q5495936$E8EDEB1E-0239-41F0-8758-4032FFF37A88","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ddbcb2073b5c7b755f2e5b673e59622629e687d7","datavalue":{"value":"proof assistants","type":"string"},"datatype":"string"},"type":"statement","id":"Q5495936$F3CA505B-B5C9-4146-B47D-CED0E19490E9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"61439d791f6aac729372268f16b553bcf47e3b78","datavalue":{"value":"SMT solvers","type":"string"},"datatype":"string"},"type":"statement","id":"Q5495936$B2680712-DF43-4754-8839-A22D1899817F","rank":"normal"}],"P1463":[{"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":"Q5495936$7DDB1AF8-ADB6-4943-A7F0-896AC38DF358","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":"Q5495936$CBA1D368-752A-42E4-91EF-8E44A5704C8F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"8376bcc90e7c7f009563b97a4560743162f2cada","datavalue":{"value":{"entity-type":"item","numeric-id":22158,"id":"Q22158"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5495936$752BA981-BC7C-4417-83A6-9F52FCE3AD7E","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":"Q5495936$69DBA87F-B245-45B4-B305-DE886932FBD9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"b222922e2b373ab7fb2b7a049f9de07c755ee255","datavalue":{"value":{"entity-type":"item","numeric-id":16770,"id":"Q16770"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5495936$5FA6496F-F943-4DFB-936C-E021BAB33E2F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"bcaf3b20cd7fd897f2f47a708bad9d4f554cb6fa","datavalue":{"value":{"entity-type":"item","numeric-id":14553,"id":"Q14553"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5495936$390CA7DE-13EB-4992-8FE5-B68C839AF427","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":"Q5495936$E27C26E1-5637-4AA9-BEC5-ABB28A78EAE9","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"718b7a4ded4a3edc982e6611b6bae8075f8987fe","datavalue":{"value":"https://doi.org/10.1007/978-3-319-08434-3_27","type":"string"},"datatype":"url"},"type":"statement","id":"Q5495936$4B65CF4C-1E51-4C0F-AD4D-966EF3182AF1","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"cc9db16f26bc28a3bb86ed4435b99408c040d8d0","datavalue":{"value":"W119865360","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5495936$0139777A-C3FF-4DEC-A9D0-E45C4F6032A8","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"f660261386a269c5c6d007e1774c790f4ddf72ec","datavalue":{"value":{"entity-type":"item","numeric-id":5815602,"id":"Q5815602"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5495936$5EEC95D0-989C-4BDC-B97D-04368583DDDE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"836ad2a04f82225da478ca9f694f5cd99360b315","datavalue":{"value":{"entity-type":"item","numeric-id":4198056,"id":"Q4198056"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5495936$AF7B2F99-A8FF-48A4-970D-D8A69ABED588","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7d9190693f3924b86be7203c014f0b8b161bc6f8","datavalue":{"value":{"entity-type":"item","numeric-id":5302559,"id":"Q5302559"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5495936$829EF810-FEB7-438C-9E14-0AA2CDF46714","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":"Q5495936$4CDBCCCB-8840-40B2-9DC1-DD7EFE9814EF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a6af1483960b5acdfcc7fab2e7274bf3ab4268fd","datavalue":{"value":{"entity-type":"item","numeric-id":4928443,"id":"Q4928443"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5495936$9CA9A7FD-E2A2-40CA-A931-4570F9B10F6E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"692645ba0e13e1ab798946ded35053c7569206ce","datavalue":{"value":{"entity-type":"item","numeric-id":2907348,"id":"Q2907348"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5495936$22942998-2F28-4881-B4E2-270E23CB96CC","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":"Q5495936$5100E7C8-15ED-4D73-9549-8F24EF49F094","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b5a256449611c84a11b081fc6ab121a5b321e50f","datavalue":{"value":{"entity-type":"item","numeric-id":1945902,"id":"Q1945902"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5495936$002A9DEE-5075-4FC6-9976-17ABDC6F7AC4","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":"Q5495936$2C4D6020-A8C3-4FA4-B2BE-641843D8F005","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":"Q5495936$43E6CF3B-4597-49B8-92F9-70866F0A5F8A","rank":"normal"}],"P1643":[{"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":"f4a322e5b5166713a5de1fc9d0d1ec7c99446477","datavalue":{"value":{"amount":"+0.8813499","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5495936$F9F71E9A-7E5A-4CEA-A720-D07649FDBF27","rank":"normal"},{"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":"8dd9e29bcd2ba6c27a49595398597f1900eecbe5","datavalue":{"value":{"amount":"+0.8730942","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5495936$7B1D2A39-BB24-4816-92FD-EA4DB7CA2A9A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"275043e7e8c4e5297664f978b9aa57e55ead1d08","datavalue":{"value":{"entity-type":"item","numeric-id":3781732,"id":"Q3781732"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"866c52c51cf69cbfaaf26c5d06b989b1d2904142","datavalue":{"value":{"amount":"+0.8652057","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5495936$78B7D288-96A8-4FBB-A824-AC42FC119E19","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1d58b013c3497a81753f3a27ec5d4fd9a1243ab7","datavalue":{"value":{"entity-type":"item","numeric-id":865631,"id":"Q865631"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"15d58d11c8a38729ce9f95470c469b80166ccb89","datavalue":{"value":{"amount":"+0.8609262","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5495936$018F1454-901C-4B9B-ABF7-CA693BC77692","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6706f674745437a28e826927d52883b093061b9e","datavalue":{"value":{"entity-type":"item","numeric-id":2988387,"id":"Q2988387"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1f74b58477588501e271906604edf28c7b6ac61d","datavalue":{"value":{"amount":"+0.8475689","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5495936$32B12042-2ED5-4401-A766-A88DA2B2ADEB","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":"de05c714623caab33b3b31041a99a4c6bfccc5f2","datavalue":{"value":{"amount":"+0.84178823","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5495936$A2846BB7-EA56-480E-8316-B75AD9AA7611","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8e7c6885db120465d3fc977ee01677784fd7b685","datavalue":{"value":{"entity-type":"item","numeric-id":3809309,"id":"Q3809309"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6b8309407127679ae0e2b455bcef9541e7b6a6f4","datavalue":{"value":{"amount":"+0.84077555","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5495936$E9E5E816-0C23-4EDB-BDD4-4516C68F230D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2bedcca7522067bd4c9657d84c45f2b6bd8d3026","datavalue":{"value":{"entity-type":"item","numeric-id":1272613,"id":"Q1272613"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ae74d81350a4e4b0371565d2d49a30e13809dec8","datavalue":{"value":{"amount":"+0.83953416","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5495936$E35230FD-DBDB-463C-B44E-B7BEB6B752FB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ab7e5fbdc6c2b3a12f649e72dff75f5485ad2e9c","datavalue":{"value":{"entity-type":"item","numeric-id":286803,"id":"Q286803"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"332df745bd028e8e77c3b43bc0502686424ada9c","datavalue":{"value":{"amount":"+0.8392107","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5495936$8F10A8D4-5408-4AC2-92B4-C0F318E8813C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"448d3fdd2fd865cda8d1d7b2b7d42246a159d8f3","datavalue":{"value":{"entity-type":"item","numeric-id":831930,"id":"Q831930"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"fe911c6920a77067da9a2a4d8777bab6ba3dff95","datavalue":{"value":{"amount":"+0.83918226","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5495936$B61456AF-C51E-4635-8AD4-403AED90F1B9","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:5495936","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:5495936"}}}}}