{"entities":{"Q4647515":{"pageid":6677096,"ns":120,"title":"Item:Q4647515","lastrevid":97925117,"modified":"2026-06-05T15:49:20Z","type":"item","id":"Q4647515","labels":{"en":{"language":"en","value":"Presenting machine-found proofs"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7001908"}},"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":"Q4647515$187B688D-AC32-421F-B9F5-594C2F6D2C1E","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"f77e07ffabcedc110d51d33e96d80f4bcd2ab1b5","datavalue":{"value":{"text":"Presenting machine-found proofs","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q4647515$9508A5FB-AC96-411D-A8A2-D03F277FE9A3","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"bdc700e6ad534f031bc65a7bcd4669a5fcd3c36f","datavalue":{"value":"1412.68235","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4647515$F6A8E17F-CFC3-48C1-8AC4-F98B92CC1439","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"58db7cb85e3f91e786ea388c828a5a63945c55ed","datavalue":{"value":"10.1007/3-540-61511-3_83","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4647515$782F0712-D7B2-4251-8B99-1603855816F5","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"1ba60eb652d97326dd4692eecddf33b290fb23dd","datavalue":{"value":{"entity-type":"item","numeric-id":1277341,"id":"Q1277341"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647515$5298D674-6B8E-41E3-9257-5818FB401992","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"9d967be3a064d3a539902cfc5014c43e64cf1ea6","datavalue":{"value":{"entity-type":"item","numeric-id":2779420,"id":"Q2779420"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647515$FC6C3F97-B8D4-484C-BFDA-5CD7645A35A0","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"1c1c5ae1cd90ac8f2e7ae6528ac21a720bbd1fe8","datavalue":{"value":{"entity-type":"item","numeric-id":4647495,"id":"Q4647495"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647515$BCEDF18D-C3A2-4BE4-A38E-E97D0A007C5D","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"250f083a2ef1e7a7df79afad0acdd22e5799ecf5","datavalue":{"value":{"time":"+2019-01-15T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q4647515$E9372A73-C71D-431B-B508-B78FC04DBAFF","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"fb8f7939b137b91420aa9818ffa31c83c25d17d5","datavalue":{"value":"http://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:hbz:386-kluedo-2086","type":"string"},"datatype":"url"},"type":"statement","id":"Q4647515$98CB79CA-39BB-4A0C-BD1D-91E47B7F0549","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4647515$177C2076-21DA-4B03-A9DA-EF8A23E76DC7","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"8c747de27964d1b083c0aeca8d2d605a34aa4988","datavalue":{"value":"7001908","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4647515$5339C60B-DE62-422F-8E63-12E3CE53BD85","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a7245057d33d9a959e820bafe53b372c083536e6","datavalue":{"value":"natural deduction","type":"string"},"datatype":"string"},"type":"statement","id":"Q4647515$16D0F01F-2316-4985-B68E-6C5F8CA7B462","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"6aa75b0cf12c21394129a09cf91fa52d44d00338","datavalue":{"value":"intermediate representation","type":"string"},"datatype":"string"},"type":"statement","id":"Q4647515$1EA3AD26-5F44-4CC7-8B6E-702C14ED19FC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d94aa70de485eb44f73e6afe9a7c9619ece73173","datavalue":{"value":"mathematical textbook","type":"string"},"datatype":"string"},"type":"statement","id":"Q4647515$752AB750-2730-4238-AF57-04335AEC5D65","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e2bcc0f680649b9a61988f572aee71077073d057","datavalue":{"value":"linguistic resource","type":"string"},"datatype":"string"},"type":"statement","id":"Q4647515$4370AE67-F43F-4108-8332-12B72DE05FA5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"80008d81258ded70d575e02944a82647618843a1","datavalue":{"value":"resolution proof","type":"string"},"datatype":"string"},"type":"statement","id":"Q4647515$40A59553-D8F3-4270-814F-40F48470EBA8","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"0fea2f9619de059473275bc7b30252f10595c358","datavalue":{"value":{"entity-type":"item","numeric-id":41387,"id":"Q41387"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647515$D833DFE3-6DB3-4D67-930C-CE2D79F09B70","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":"Q4647515$7A5299F7-6B98-4B73-BFA8-CD33805DA7AA","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"efeb73acec358c524a63dc4fec9763a6cb4359fa","datavalue":{"value":"W2155990634","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4647515$2A78A478-87D5-46A9-AC58-8E527F506158","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"a74c52dce2b41371b695c2dd9e16f460a2c3a87e","datavalue":{"value":{"entity-type":"item","numeric-id":3880316,"id":"Q3880316"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647515$4F49155B-B731-4252-9F8F-36ED3160322C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1a44e30561cc2aee4aee48347e083f603add9dea","datavalue":{"value":{"entity-type":"item","numeric-id":1228369,"id":"Q1228369"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647515$338F5A9A-F4C7-4DD8-AA74-41426C4E4C86","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5e74a7a357b1b46dc042b2194329594218f6b370","datavalue":{"value":{"entity-type":"item","numeric-id":1840142,"id":"Q1840142"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647515$9DCAD4A8-544B-4DC9-9881-4E3697A4E7D2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c3651c6ae0eff448b9c689ee43459c1ff0bf16e9","datavalue":{"value":{"entity-type":"item","numeric-id":5210809,"id":"Q5210809"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647515$0B147E88-5DED-474E-BA62-65D93F7DDF88","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0e676da38d777563663597edd24cfe10db73770b","datavalue":{"value":{"entity-type":"item","numeric-id":3490999,"id":"Q3490999"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647515$EA4615BC-307C-4B84-BBB7-94D7D4D447B8","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b589f87e4db1a7c1e984bb6fbd0ec08caa2daf74","datavalue":{"value":{"entity-type":"item","numeric-id":5122009,"id":"Q5122009"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2bd482f03f39be496c8b0efa7c19938cbcfa7adc","datavalue":{"value":{"amount":"+0.9017","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q4647515$430574F0-CE5E-4AC4-BC13-8106CA4B6A6D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"72684c9b287758706928e3c04d081a42aeb9d9b0","datavalue":{"value":{"entity-type":"item","numeric-id":4342457,"id":"Q4342457"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"be84d016db2a7162e3a6cb4a1f96cba48da8b9cd","datavalue":{"value":{"amount":"+0.86425394","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q4647515$080B7795-227E-493B-8563-52282833B674","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":"8df0e4cc18e387f71e5800c24cdc3096f5967886","datavalue":{"value":{"amount":"+0.85606265","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q4647515$547A89D3-75E8-4234-BF5E-2ADCC6B4C523","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b8a5d18780a3dbdb4959fbe9fb76a2b4792c26e8","datavalue":{"value":{"entity-type":"item","numeric-id":3490999,"id":"Q3490999"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8837e76953a47045c34413bdeaa8394bd673c053","datavalue":{"value":{"amount":"+0.8533669","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q4647515$26B9D064-4C23-44DE-84A3-40553C1758C3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"de10203981c5068b0631b8004c64b7ff2f0e4f00","datavalue":{"value":{"entity-type":"item","numeric-id":4818803,"id":"Q4818803"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"201120e8792ce214caa1454e4f1b713a18c7f631","datavalue":{"value":{"amount":"+0.8519453","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q4647515$46C6456A-E216-4DF0-86DB-9D628994B6FA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"64aee88bdc774d47038cd0b81eb9298c5b3d52fe","datavalue":{"value":{"entity-type":"item","numeric-id":1124588,"id":"Q1124588"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6242d65e00f592a814294d77b44caac53e508162","datavalue":{"value":{"amount":"+0.8476251","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q4647515$820EA7D5-41BC-46CE-9CFC-A849E5CE1C10","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"112842c88f015f833c53696a3e75c28ba693beea","datavalue":{"value":{"entity-type":"item","numeric-id":5384148,"id":"Q5384148"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"bfccfa2861f52435adc104a856e433e24a3c3ac5","datavalue":{"value":{"amount":"+0.8463106","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q4647515$7C75EC4D-9DF1-4493-8840-2A61C3F75F72","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c636da3f6df0db98ad3898751b71d2c79d534186","datavalue":{"value":{"entity-type":"item","numeric-id":3690258,"id":"Q3690258"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4843f315450d4c9727480961a0c096e5a6de7d9f","datavalue":{"value":{"amount":"+0.8455502","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q4647515$7D6C0EB0-B8C9-49D5-8A3A-10C351EEEE95","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3ad52f58547ab0810a180a2de1a917115feb0246","datavalue":{"value":{"entity-type":"item","numeric-id":4381418,"id":"Q4381418"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"36ab7578b2af589675115b92297a1da6e00ebd6c","datavalue":{"value":{"amount":"+0.8417608","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q4647515$69B527BB-4ECC-4A6A-99DC-6CDBC0161805","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Presenting machine-found proofs","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Presenting_machine-found_proofs"}}}}}