{"entities":{"Q1319391":{"pageid":1330141,"ns":120,"title":"Item:Q1319391","lastrevid":70132227,"modified":"2026-04-13T12:39:37Z","type":"item","id":"Q1319391","labels":{"en":{"language":"en","value":"IMPS: An interactive mathematical proof system"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 549833"}},"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":"Q1319391$BF2C3817-377C-4D91-AD49-700B641823C7","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"77c59132d7fb0bc943c52b157f98233b3e3e3229","datavalue":{"value":{"text":"IMPS: An interactive mathematical proof system","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1319391$E4AF1B54-2582-4BEC-83E1-B82A03D31EE8","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"ad0a37f61a4a9b861697bc80c5f2a1bfb1bcfd28","datavalue":{"value":"0802.68129","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1319391$0AA8CB64-6F6E-4D93-BA93-88527020B0E8","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"1b80a7383242173fa861d83fb63c55984faee4bc","datavalue":{"value":"10.1007/BF00881906","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1319391$CD85D4E4-3C75-40DE-92AB-60A5CC69E351","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"24d2f620d2974ebdd1015229debd06431f4c7398","datavalue":{"value":{"entity-type":"item","numeric-id":1294575,"id":"Q1294575"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1319391$F79C9A65-DB01-4ABE-8511-58E1D5F4BBE6","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"b84cc8b5923f45dc86ae69f67f68bf56d7ecfce9","datavalue":{"value":{"entity-type":"item","numeric-id":174771,"id":"Q174771"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1319391$B8DAFA28-29D8-40C1-8EE4-3D053FD8D58A","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"43a82918b7cb04f59437503b817f00af9741808a","datavalue":{"value":{"time":"+1994-04-12T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1319391$48613F30-6F62-4BD2-927E-9E5C133BA0E9","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1319391$9C08763B-6055-4CCC-81AB-BA45959172F5","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"52183c7019bd5e4fc7606bbcf0a6ed4f4fc362ab","datavalue":{"value":"549833","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1319391$BF602C4D-4C30-4A70-8311-1E212093EF1B","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"21cf102e52d55bb9e3ba4ca1c32b8839281988dc","datavalue":{"value":"interactive theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q1319391$06BA8EFA-7742-47D9-930A-9362F1A80D52","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"6c9ea3d35f336e43b1f0c691430f17ba5ced6933","datavalue":{"value":"automated analysis","type":"string"},"datatype":"string"},"type":"statement","id":"Q1319391$1542338A-2FCE-4712-8F66-D66907A1DFDE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"6321342a39642c67b7392123e6179d55b8ae28b6","datavalue":{"value":"computing with theorems","type":"string"},"datatype":"string"},"type":"statement","id":"Q1319391$937AE77B-0525-482C-94A7-54C6404E6AC5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"095e2bcb3504c26c43b06f39058ae01811566e3d","datavalue":{"value":"theory interpretation","type":"string"},"datatype":"string"},"type":"statement","id":"Q1319391$6490092B-3EA8-490E-BDF3-ECF3AB1E053C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"39810ec381ba48fb5861c168391fa7d328efd8b1","datavalue":{"value":"higher-order logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q1319391$FF919E6D-DE88-46D6-A71E-F29FD8BF3636","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d31be1229374545ff94fd95ad2a5ce9870f120db","datavalue":{"value":"partial functions","type":"string"},"datatype":"string"},"type":"statement","id":"Q1319391$F3645BA4-4802-416E-93FC-C94A96817880","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"1aec27d540e360c78ddad230e6e300ced62bdec3","datavalue":{"value":{"entity-type":"item","numeric-id":18433,"id":"Q18433"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1319391$F6B35074-96E1-408F-A3F4-1FFB6C7F4A59","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"29391b19386946f3f8609d95651483db905027b9","datavalue":{"value":{"entity-type":"item","numeric-id":22439,"id":"Q22439"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1319391$8A24CF8F-75B0-43C2-9332-D1E8BF1C4984","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":"Q1319391$F8BDA099-DEAA-49E1-8B0A-D840634E1B6F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"7f231912461a4cf859d87b4356c5e2a2037e1e84","datavalue":{"value":{"entity-type":"item","numeric-id":17631,"id":"Q17631"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1319391$3DDDBE95-019F-4473-894F-839F916F6BF8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"2e07b63a7544a6d7c83390f82ddae368b77e124c","datavalue":{"value":{"entity-type":"item","numeric-id":19570,"id":"Q19570"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1319391$A965BD94-98A0-4865-811B-A6963F1983AA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"9c40cf9a35904f638a7cabef2bc178bad46391f7","datavalue":{"value":{"entity-type":"item","numeric-id":13717,"id":"Q13717"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1319391$79DB9911-83E4-47F9-9B00-CFC4AFB02714","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"27b6ae20da44d6f09b655d9481cc0df08a8ffcdf","datavalue":{"value":{"entity-type":"item","numeric-id":18826,"id":"Q18826"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1319391$D1787EFC-AD05-48E0-AA37-B97EB87BE338","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"0252b90583a3720591e1bcebade6d086a9b1ed2a","datavalue":{"value":{"entity-type":"item","numeric-id":40607,"id":"Q40607"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1319391$49A0DFEC-2BB3-4E90-A71A-AE28DE5E4496","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":"Q1319391$859FF56A-0081-462C-9213-804A460814F8","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"85b58e334bbf84629d414ca7d6688164e5524fe2","datavalue":{"value":{"entity-type":"item","numeric-id":4726218,"id":"Q4726218"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1319391$903D08D7-2B53-4AD8-830D-9BDE2D146846","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4a30605f1ebdbd14040c016d942a5c6190434145","datavalue":{"value":{"entity-type":"item","numeric-id":3709919,"id":"Q3709919"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1319391$584E9BD2-2860-4054-94B5-96978CA7FEFD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4ca7e027091589776f78a6d7ad8457e805c17b28","datavalue":{"value":{"entity-type":"item","numeric-id":5777498,"id":"Q5777498"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1319391$F3ACD287-7EFB-4EAA-BCD9-185A7B75AEC7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2d592f87e8857ff4d106dd1dd178161f50c9229b","datavalue":{"value":{"entity-type":"item","numeric-id":1108266,"id":"Q1108266"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1319391$95A5E83F-41F7-4C52-84D8-CC6D638025B6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c03b1b7c54fac5621448e5c427c845de6ebfbec4","datavalue":{"value":{"entity-type":"item","numeric-id":3281164,"id":"Q3281164"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1319391$F86A8D1C-6EAF-450D-BB82-5DE7A129A513","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5ca4f823ca2e82e86e612699cdb65f38c133999d","datavalue":{"value":{"entity-type":"item","numeric-id":4052071,"id":"Q4052071"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1319391$8BDFD978-461E-40AD-8027-422FE54CA277","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3e469695a6ccdc7d8268978ac58e95413371ff1c","datavalue":{"value":{"entity-type":"item","numeric-id":5753924,"id":"Q5753924"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1319391$DA8B27D9-6C81-4C04-84E1-4AD99B961329","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3af6d79cb7627680af279f9390de4528d7005030","datavalue":{"value":{"entity-type":"item","numeric-id":5344166,"id":"Q5344166"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1319391$16A61C5B-11F7-4EF8-857F-9C60EEE756C8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ca897a8c41bcaa8d142a48f17d1f2b052c9612d2","datavalue":{"value":{"entity-type":"item","numeric-id":3332238,"id":"Q3332238"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1319391$05D7A3BA-E959-4574-A3A7-A67BDBDAC585","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5dbdd618fcd9894cc43913fda0ef46a6ceb0f2e1","datavalue":{"value":{"entity-type":"item","numeric-id":5798021,"id":"Q5798021"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1319391$224A5A97-B4C4-4BA0-BB07-58998A3DFC0A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2bbe63c42c351a315dabe14e649afaf16535549b","datavalue":{"value":{"entity-type":"item","numeric-id":4255519,"id":"Q4255519"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1319391$C4D93052-4D99-4E5C-A281-0FD65F3A8442","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"009122af7eb8e6ecc8feb2892d4b88e663912c90","datavalue":{"value":{"entity-type":"item","numeric-id":3328540,"id":"Q3328540"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1319391$804EE62F-F7FE-4558-8F04-52F9F92BDB03","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c4ceaa295163b971ae499531a20e1ec0863c4f76","datavalue":{"value":{"entity-type":"item","numeric-id":751642,"id":"Q751642"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1319391$2FA73136-DE2A-495C-A99F-E7F6AE54C189","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2fa762974e3cb0286b2a40e5214b429aa00cb948","datavalue":{"value":{"entity-type":"item","numeric-id":1217684,"id":"Q1217684"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1319391$25955BFF-8EC7-4BC4-8390-2FE71C6AEE9A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"63f891712b7d48896da4510dee1617284577b50f","datavalue":{"value":{"entity-type":"item","numeric-id":3727947,"id":"Q3727947"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1319391$3BC049A8-5003-483A-B885-499357F8776E","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"e7f36c72ce0c165d56796bd21bd840573425b0f5","datavalue":{"value":"https://doi.org/10.1007/bf00881906","type":"string"},"datatype":"url"},"type":"statement","id":"Q1319391$6F175B4C-E1D0-422B-9396-A346C4B14AB2","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"dc87e0ec8002b11a9556b8787e02d90adcfbf6e0","datavalue":{"value":"W2137810559","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1319391$F6DCBF32-8F1F-4DCE-97C8-35D518BF442E","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c06bccad4409f00374fa4a8a87e8e5bb57dec492","datavalue":{"value":{"entity-type":"item","numeric-id":1798938,"id":"Q1798938"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"acdbe163ee772b8e70bf14288dd8acffef5c1c6d","datavalue":{"value":{"amount":"+0.8058243989944458","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":"Q1319391$98440A3D-638F-4069-8E49-B2B78BFA596F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f62d3c74f1452c00e4d697b29b4b03afa7c01b35","datavalue":{"value":{"entity-type":"item","numeric-id":865629,"id":"Q865629"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2cc33c7ceae25309f65389957e221a13fc830c4e","datavalue":{"value":{"amount":"+0.7806928753852844","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":"Q1319391$43966C75-97E5-4907-BD82-5097A654943F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5e4aceb89ded0586b4466107863cec1384fd4019","datavalue":{"value":{"entity-type":"item","numeric-id":1314643,"id":"Q1314643"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1bb7d650283513adb1b7e46825a9394beed75278","datavalue":{"value":{"amount":"+0.7592245936393738","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":"Q1319391$E584EF60-0991-40DC-9E80-966E58BDBBD3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"027e66e493294de396e3f06701b232a3660c5eaa","datavalue":{"value":{"entity-type":"item","numeric-id":1823013,"id":"Q1823013"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5450078dddb643a7e8cd770b0090c1040624b844","datavalue":{"value":{"amount":"+0.7519784569740295","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":"Q1319391$693D830C-CB9E-4E0B-BF84-8935224D1965","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3b168262f9e1b4514313a24dfabf8223d2ad31a3","datavalue":{"value":{"entity-type":"item","numeric-id":556682,"id":"Q556682"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0e762978793c33b0b9964a877411a02887df6d28","datavalue":{"value":{"amount":"+0.7479771971702576","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":"Q1319391$6D859625-B24F-4E2B-9575-47813024FB85","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"IMPS: An interactive mathematical proof system","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/IMPS:_An_interactive_mathematical_proof_system"}}}}}