{"entities":{"Q5875449":{"pageid":7905000,"ns":120,"title":"Item:Q5875449","lastrevid":93267644,"modified":"2026-06-05T04:06:30Z","type":"item","id":"Q5875449","labels":{"en":{"language":"en","value":"Declarative Proof Translation (Short Paper)"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7649984"}},"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":"Q5875449$2C49ED60-1000-431D-AD6D-8D0DCF3AABBF","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"6ad6a046b48bbe4ab777309f1d5c19b5fc7dfbda","datavalue":{"value":{"entity-type":"item","numeric-id":286799,"id":"Q286799"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875449$33DF9649-BF9F-4DE0-B9D2-B7DAD52EBF92","rank":"normal"},{"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":"Q5875449$D70253C3-2A8C-4813-9A0B-4DFBCD761706","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"6695abe38664d65c38747de7b5fe54d9caa92dea","datavalue":{"value":{"time":"+2023-02-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":"Q5875449$61170295-7B41-45D4-A5C6-5FF5F052FC2A","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5875449$E8BA2AED-2111-473F-BF3A-509CC03E4807","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"66ee7943e278ca4e25f211ca12f0b915150e44dd","datavalue":{"value":"7649984","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5875449$23DC038F-29AE-4ADC-92D6-2FD181896FD0","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1ff490775ddfb66736a92a70c9f4b7d7e8e09869","datavalue":{"value":"declarative proof","type":"string"},"datatype":"string"},"type":"statement","id":"Q5875449$9017F74C-A5E1-48F0-AF8F-0180F9B10338","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"14a6728e50cbaca75cf287bc48ae14f636315ae3","datavalue":{"value":"translation","type":"string"},"datatype":"string"},"type":"statement","id":"Q5875449$30CCB966-ADDF-4173-B20E-D351AD8FD5A2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"481790dcea94161f0646db7f365d04cfdf86f5d9","datavalue":{"value":"Isabelle/Isar","type":"string"},"datatype":"string"},"type":"statement","id":"Q5875449$6DC71E48-CFD2-4875-B962-23C10D54526E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"571c0e1fb7a78a4a545c4f12cd6536c1efe33bd7","datavalue":{"value":"Mizar","type":"string"},"datatype":"string"},"type":"statement","id":"Q5875449$38CB0D95-B2B6-4C68-8DA2-7A1645AF09F0","rank":"normal"}],"P1463":[{"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":"Q5875449$0D6CC685-F6BE-4F5F-8981-A704BC4AD5B8","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":"Q5875449$510D83B7-9081-4FC2-8EB3-08D631EFAC08","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"39d1d25ae8c00cfad058b188db36fd61dac09925","datavalue":{"value":{"entity-type":"item","numeric-id":27041,"id":"Q27041"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875449$750EFD7B-1C87-4EB6-9CCC-320B308EF3A0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ab6ee58efeeaa685ac2b8ecf828badcfb673e8c7","datavalue":{"value":{"entity-type":"item","numeric-id":12929,"id":"Q12929"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875449$434FCFAB-A1CF-4502-8AA5-A5B6DA91220D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"4e22b8176489c2409392314db08f466f9ad9c934","datavalue":{"value":{"entity-type":"item","numeric-id":30463,"id":"Q30463"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875449$651ADA08-1617-48BD-8A78-DC845886C261","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":"Q5875449$B7CADC48-F547-47AA-A35F-D7C18C2B8CAB","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"4fa280729aba7cb8724bbf8207c6a4442deb2c4d","datavalue":{"value":"https://doi.org/10.4230/LIPIcs.ITP.2019.35","type":"string"},"datatype":"url"},"type":"statement","id":"Q5875449$45F18381-3518-47CD-AD5B-DA92A33846BC","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"66a1ae98f0dfe20931d5da9cb03c0a7dd9c3b2a6","datavalue":{"value":"W2978888779","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5875449$6A59C89A-86EE-485D-8ECE-4FB1C112AE17","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"6a40a27f3487586fe4c8f04e68cbaf63f12d6e24","datavalue":{"value":{"text":"Declarative Proof Translation (Short Paper)","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5875449$37D1C3F8-94E8-4DE5-85E8-4DB7BA03D9FC","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"b5a5f605a610fb0894190f2fe71d26b5d54433f3","datavalue":{"value":{"entity-type":"item","numeric-id":5195266,"id":"Q5195266"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875449$55955EF7-35EA-4FB8-9593-0E256CB0D8F0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2ebbe3f6a88e51e1203c3c8190dcfbdac3cc8dde","datavalue":{"value":{"entity-type":"item","numeric-id":1663215,"id":"Q1663215"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875449$B415FB0D-1EED-4126-BDE1-B37B1C07FCCE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9b06809062082b8f9f5dbc080e3987837376fa3d","datavalue":{"value":{"entity-type":"item","numeric-id":3499750,"id":"Q3499750"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875449$FAD3128C-DAC0-4A71-AF3B-30FBDCB3BF69","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8242928870aab67343ad0152eb7ca8357168f7f3","datavalue":{"value":{"entity-type":"item","numeric-id":3454108,"id":"Q3454108"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875449$B5005F0D-5069-48A2-8AF7-22D3EFC7CAA0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d861948f1f6146a05d3ce13e4c51b6e0c074be1f","datavalue":{"value":{"entity-type":"item","numeric-id":286794,"id":"Q286794"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875449$DB4CF911-A365-43FE-A4D6-0CA263974C6A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4465a27d995e35d0f84f566c2db9a02e2a007418","datavalue":{"value":{"entity-type":"item","numeric-id":1798961,"id":"Q1798961"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875449$DEF1E102-901B-490E-81B7-6EB56777E0DA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d3664b6907ca78dcc7471c19ca41bf9ba07ff81c","datavalue":{"value":{"entity-type":"item","numeric-id":2323445,"id":"Q2323445"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875449$F0D33BF7-3316-43F5-99C3-F59C6575B8DA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c0f03bf183c7a653e5e84320e58ed58d37b137b2","datavalue":{"value":{"entity-type":"item","numeric-id":1868515,"id":"Q1868515"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875449$AEC2FEA3-2572-497B-BC56-7D571948C54F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"502ad8224b7ee39a96e36cfcfba1b8b740baa8c6","datavalue":{"value":{"entity-type":"item","numeric-id":4790672,"id":"Q4790672"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875449$B03C36F1-C928-402D-8BDD-A5DFE5EC08AB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d4ef8738eccd7b653460e41e83660d0f8b8c95df","datavalue":{"value":{"entity-type":"item","numeric-id":2881098,"id":"Q2881098"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875449$C32D801C-209B-4EB5-A9A6-63161ACC6FA7","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"16a60fed036e554a86f476a44f0bafc55b923027","datavalue":{"value":"10.4230/LIPICS.ITP.2019.35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5875449$9456EC98-0A1C-4CC5-9046-466B2C589EB5","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Declarative Proof Translation (Short Paper)","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Declarative_Proof_Translation_(Short_Paper)"}}}}}