{"entities":{"Q1675786":{"pageid":1686527,"ns":120,"title":"Item:Q1675786","lastrevid":52948721,"modified":"2026-01-23T21:20:43Z","type":"item","id":"Q1675786","labels":{"en":{"language":"en","value":"A formal proof generator from semi-formal proof documents"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6802653"}},"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":"Q1675786$82D06A65-C580-4820-8B9B-F66E0AE9645E","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"5d49e9602061f025ebd4dff89e5cf0b373f1ed15","datavalue":{"value":{"text":"A formal proof generator from semi-formal proof documents","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1675786$838C5D53-AB54-4D1F-886D-2986517694DA","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"fb4b3bdb6ff5ddd4c528ce6c96190ebeafe3b559","datavalue":{"value":"1444.68287","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1675786$6A5E8E10-F1FA-4EF5-A3FF-1F1F23043EF9","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"7015266ef1453ad3ce87f3fae1a942134e8d5328","datavalue":{"value":"10.1007/978-3-319-67729-3_1","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1675786$66012805-0176-4378-B56A-638FC0831DA3","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"0b1ecda69e1cbbf3f527244edb48a622cad39ee2","datavalue":{"value":{"entity-type":"item","numeric-id":520241,"id":"Q520241"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1675786$B68B8832-B52F-4DFC-B5F0-99129AE28AAB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"19c8b8152eb049581c2538d13b0e2ff0fba8e40b","datavalue":{"value":{"entity-type":"item","numeric-id":520242,"id":"Q520242"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1675786$29985452-8DFB-48CC-8FCD-A5C1DBB3101A","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"67aba7197112cbac1f8ed2910c0f63c4d1f0c462","datavalue":{"value":{"time":"+2017-11-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":"Q1675786$47ED2463-65B6-4A50-9C4E-9D97A2978788","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1675786$91728793-8A01-4971-ADD8-404A690AA50C","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"6f00166081c5e3edd695ca4509961d4f8694098c","datavalue":{"value":"6802653","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1675786$B349615A-3108-40F9-A8B0-5E85EDA9132A","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"a9cc08f1ee64c2fc0d984a8fe54c7c857eeb0cc4","datavalue":{"value":{"entity-type":"item","numeric-id":18366,"id":"Q18366"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1675786$EAE0499D-BC58-4FC6-B9CD-248119DCB349","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ebe6f223efc2405cf071214b7d4e0e7858bf57fc","datavalue":{"value":{"entity-type":"item","numeric-id":18367,"id":"Q18367"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1675786$DEFE5EDE-7FD5-44DF-90A1-70C516AE4975","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"80ad234dc0924dda60983aa70fc106cb35f3b96e","datavalue":{"value":{"entity-type":"item","numeric-id":19080,"id":"Q19080"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1675786$81242318-3B03-4C7D-AAAF-1DA4B4C37F28","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"305c92e1b00f79e1f68085b3a6595ba8bd124116","datavalue":{"value":{"entity-type":"item","numeric-id":31424,"id":"Q31424"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1675786$562FBB20-B840-48A5-ABFE-6BADBC4813ED","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"b6da1f42e3d4d28e24ecb68672c28ee0982a60c2","datavalue":{"value":{"entity-type":"item","numeric-id":12950,"id":"Q12950"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1675786$FC1FC748-51E9-44B1-9572-18074131D290","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"fa5dc13872ba1592e71dabc4befba1daea72a8a3","datavalue":{"value":{"entity-type":"item","numeric-id":14275,"id":"Q14275"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1675786$9B5343B1-2A2D-46B1-BE56-0D58018D42E5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"c46d84e301480ba8a5854ea89c3d27b865a03eb9","datavalue":{"value":{"entity-type":"item","numeric-id":16016,"id":"Q16016"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1675786$CFFA5769-F128-4DF1-BCC3-4FAB42BDA351","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"91328e3ac5dfce9b45d01b607b8d8c272a5b6733","datavalue":{"value":{"entity-type":"item","numeric-id":14670,"id":"Q14670"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1675786$2E66F872-FCA4-44E7-9DC9-A3E52120C8C7","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":"Q1675786$9868BF33-0EE1-4068-9FAC-04AFB9ECBC07","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"bc68b17961888b89c91466ed798884974f8583de","datavalue":{"value":"https://doi.org/10.1007/978-3-319-67729-3_1","type":"string"},"datatype":"url"},"type":"statement","id":"Q1675786$A7FF7C8C-4E60-49FF-A9A1-377E780E83FA","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"6fbd62f2e6df5d9853b7c5615f972ddb8221fef0","datavalue":{"value":"W2755232768","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1675786$18656EF6-A30B-4CB3-82E2-026CE0BAD12C","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0b56e97bb40511e5826c664071220970d165b082","datavalue":{"value":{"entity-type":"item","numeric-id":2945712,"id":"Q2945712"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1b749fcebeb672fc53de7d30c8b97b68a5724d6c","datavalue":{"value":{"amount":"+0.7413005828857422","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":"Q1675786$AA3AD66C-F885-4C7A-BF66-96BEA1F38D61","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d66339c795d505f780406e18e20e0f95f8bd017d","datavalue":{"value":{"entity-type":"item","numeric-id":2729065,"id":"Q2729065"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"582eb49c61990cdec9b4e97ba40eda4a3e461bac","datavalue":{"value":{"amount":"+0.7330225706100464","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":"Q1675786$98C8765E-8612-419B-8710-F1BD91303C35","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3e74be111e7310838d3555ac536d1cf46c6084ed","datavalue":{"value":{"entity-type":"item","numeric-id":4370238,"id":"Q4370238"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4d5603599c08620ec1d9cb252a955fac96c3cff0","datavalue":{"value":{"amount":"+0.7292260527610779","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":"Q1675786$8E953855-7861-4D86-9988-7C1B2A57584E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"fd585486e94ec0405f2076172b880f2fc6e0761b","datavalue":{"value":{"entity-type":"item","numeric-id":4385443,"id":"Q4385443"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8cccd391b0beb365fa3959a8067284dcf2e583cc","datavalue":{"value":{"amount":"+0.7164229154586792","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":"Q1675786$79469EB0-5C30-4122-9931-A3993EC2839E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"19203accc4a7a22b6e0e7ded8f7f4df3e916088d","datavalue":{"value":{"entity-type":"item","numeric-id":5898512,"id":"Q5898512"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7044609a92b77d6df74a01b0a2b19e15b30e8360","datavalue":{"value":{"amount":"+0.7118707895278931","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":"Q1675786$9FA7794E-B00B-4C02-9FDA-52835FE7FA26","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:1675786","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:1675786"}}}}}