{"entities":{"Q5204800":{"pageid":7234371,"ns":120,"title":"Item:Q5204800","lastrevid":91910948,"modified":"2026-06-05T00:23:10Z","type":"item","id":"Q5204800","labels":{"en":{"language":"en","value":"Proof simplification and automated theorem proving"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7140438"}},"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":"Q5204800$5A10790E-256A-4A79-A55C-4B02FA1DDB00","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"96220f31c02164bc73224b603a377c2bdb809e2f","datavalue":{"value":{"text":"Proof simplification and automated theorem proving","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5204800$4088B47F-7869-4796-9F2D-D191F0017C07","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"c27c5b39a143fd6ed7e81786cf99567f0bbeb5c2","datavalue":{"value":"1436.03101","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5204800$31A97EB1-D9B2-4EF2-AA17-30CC80FB7176","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"a13ffa206096651a7eda5901a1abc51007a10be2","datavalue":{"value":{"entity-type":"item","numeric-id":144519,"id":"Q144519"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5204800$C33B3189-5BA3-4EE6-9494-D8E5A5B6B717","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"3f8f9cf30177c49e6797ca12be4ec0fe8e8e3eb2","datavalue":{"value":{"time":"+2019-12-05T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5204800$71C98D82-8813-4C0C-995C-BF269FD0A9F3","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"a565077d5c438aa7e6eb653637a9ff71b7342853","datavalue":{"value":"https://arxiv.org/abs/1808.04251","type":"string"},"datatype":"url"},"type":"statement","id":"Q5204800$D53CE6D3-F57D-4A0A-9D47-05CF3C48B022","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P205","hash":"0a9c3620ef84c6680375023436129d8de94b681b","datavalue":{"value":"http://europepmc.org/articles/pmc6365848","type":"string"},"datatype":"url"},"type":"statement","id":"Q5204800$ED7E1A28-47B9-4AED-BF9D-F912AE17FB0C","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5204800$85A090FE-41F3-4D65-B87F-14B87D6858BF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5204800$03491B70-D434-4158-A68D-D50646152FE3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"ece9b879f80d96e2a1d45b28bdcc8cfa6b01861e","datavalue":{"value":"03F20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5204800$071D8366-6C24-4752-9D09-905A2ABD38CF","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"eb9089550e7ad87e018b95cf3a7ee40176a8f863","datavalue":{"value":"7140438","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5204800$FABCE364-1D56-4EEE-B82C-DE00D249B599","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e97175fd5d747e7d34cbcc625e3abab53d84653d","datavalue":{"value":"automated theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q5204800$5CC9648B-325B-4E99-9F73-339E640FDC71","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"66a965629f61e84a258bd823df7588e6009022dc","datavalue":{"value":"proof simplification","type":"string"},"datatype":"string"},"type":"statement","id":"Q5204800$316D22C8-ECB4-4FF6-8AC2-9B1228FEA434","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"266db153a53e546844fc36f71b0b8a034829e061","datavalue":{"value":{"entity-type":"item","numeric-id":855330,"id":"Q855330"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5204800$B22AB5B6-46A4-43EE-83AE-5A35308CDE8B","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"1e7b4d238eeafa5b21b1ef85a0d6b8900bfdc422","datavalue":{"value":{"entity-type":"item","numeric-id":15442,"id":"Q15442"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5204800$83B1E99A-5355-46D2-A583-B3FD5B33D805","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"2207b0b201a95a431b254bcb1c01d869b9f41774","datavalue":{"value":{"entity-type":"item","numeric-id":18972,"id":"Q18972"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5204800$5F16E848-BE39-4562-950D-2405DC6073B6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"82659ddd3b24a7f3c51a78eb5f25cc1e5d64df69","datavalue":{"value":{"entity-type":"item","numeric-id":17116,"id":"Q17116"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5204800$C0C5627B-9FC3-492F-A57B-4CA5FF050D26","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"1017108dce3983431546a14c274f65bc4aaae70b","datavalue":{"value":{"entity-type":"item","numeric-id":22154,"id":"Q22154"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5204800$9E21804E-9EBA-4F76-83AC-6C84A395388E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"8c766f98bf98fe7cf06a05963cc75ed84be39ac3","datavalue":{"value":{"entity-type":"item","numeric-id":31394,"id":"Q31394"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5204800$EEBA3FE3-1A82-419C-AEEA-DEE6DCED87D2","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":"Q5204800$886F3506-AF33-4E31-864A-6A88BB940A08","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"1338051b9deee0e968ae1deebf40edb1cf6db4c9","datavalue":{"value":"Q92982873","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5204800$56267482-1957-4D6F-A378-290AFD58CC75","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"94033bcf53bfc6bf89277a78befbb328ba3982c1","datavalue":{"value":"W3102050129","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5204800$F3FE889E-C95C-4729-961A-65E7225449A4","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"751e8f0efe9ea52460668d0772ba1245a23405e7","datavalue":{"value":{"entity-type":"item","numeric-id":4416428,"id":"Q4416428"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5204800$DD1ED34D-AF8D-4C07-88FA-B795B4C50F35","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"695f0bcc78ec805ea6d055a662469fc69983c828","datavalue":{"value":{"entity-type":"item","numeric-id":2759004,"id":"Q2759004"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5204800$CB651A01-818D-4328-B9A8-4FF2B5BA480E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9934e7f4b0df4e6f10eb445af518fdfeaa497f21","datavalue":{"value":{"entity-type":"item","numeric-id":1869614,"id":"Q1869614"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5204800$B60784A0-E0C5-4C63-A884-3817098E5D1F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"01894cb4c186ca51ffd95e0ed24fd5ce8f5fda71","datavalue":{"value":{"entity-type":"item","numeric-id":5951526,"id":"Q5951526"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5204800$FED302F0-DDEE-4AB3-AD5F-CD361557DDE7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"dcc0087ce4089384c4785d0cbf79970d7d51a928","datavalue":{"value":{"entity-type":"item","numeric-id":4443194,"id":"Q4443194"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5204800$0C268890-9DFC-4CDA-9EA8-35279252E1AB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"dc86c9a5df2a48a5197a520d72844b4cc69b52b4","datavalue":{"value":{"entity-type":"item","numeric-id":1272613,"id":"Q1272613"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5204800$9FC419AC-EBE1-410B-A921-FE7DC73BD24A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1d369cdefe0a9566736c1e54a3297e9cc957d72e","datavalue":{"value":{"entity-type":"item","numeric-id":5951528,"id":"Q5951528"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5204800$98897FD8-B27A-438B-882B-A864E471F237","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a4e1a291ac3cde8edb33ae306339a64d5e53ff45","datavalue":{"value":{"entity-type":"item","numeric-id":4792019,"id":"Q4792019"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5204800$5A4C7795-F522-4C91-A589-136FA867C630","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"b931ec567e8e80e704fd9d8098a0386d39108483","datavalue":{"value":"10.1098/RSTA.2018.0034","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5204800$DE2AA9CC-FCE9-45F8-B3CA-8436A770D720","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f431186fccf82fa696a1a9038fa55a84616b63f0","datavalue":{"value":{"entity-type":"item","numeric-id":5204801,"id":"Q5204801"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7f2c07f342afd60d5b979970321f959ed9671348","datavalue":{"value":{"amount":"+0.7991517186164856","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":"Q5204800$E68F953A-F8D0-48F8-88B9-ACDE5F1D2DEE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"230a18b52f7b699672fbe6879724b84dfa9849f4","datavalue":{"value":{"entity-type":"item","numeric-id":4443194,"id":"Q4443194"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0b38898b76ee46065526b04cc1b6d55f26ee4d17","datavalue":{"value":{"amount":"+0.7913459539413452","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":"Q5204800$17DA30EE-D547-4D23-A4D7-4979D084EE1A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"dda344dc59111ebdc243aa7385d8c420b1f3686d","datavalue":{"value":{"entity-type":"item","numeric-id":2767011,"id":"Q2767011"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d7d30a52a89e2a156dfcc7dc4f0b93dad9f9516b","datavalue":{"value":{"amount":"+0.7784594297409058","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":"Q5204800$A5D07EB1-14B5-424C-BC19-57982E3B64EC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ef6df3dc69f94cca2d41ddbec8ebe7923c2d43e0","datavalue":{"value":{"entity-type":"item","numeric-id":1869614,"id":"Q1869614"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"af60a8f01b61cfaab7fae8ed8335c4973cfd4b04","datavalue":{"value":{"amount":"+0.7781705856323242","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":"Q5204800$A3650796-090A-4210-9229-29E8BC3ED4C2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"239e9cc47417fe356132f0300d7025f42b281036","datavalue":{"value":{"entity-type":"item","numeric-id":6488544,"id":"Q6488544"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"65a222e33db822201a5b0058a24e260eaecc8171","datavalue":{"value":{"amount":"+0.775044858455658","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":"Q5204800$76774C45-4602-4B43-B554-99F097C15BA1","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Proof simplification and automated theorem proving","badges":[]}}}}}