{"entities":{"Q287361":{"pageid":289128,"ns":120,"title":"Item:Q287361","lastrevid":60714741,"modified":"2026-04-10T18:41:20Z","type":"item","id":"Q287361","labels":{"en":{"language":"en","value":"Self-formalisation of higher-order logic. Semantics, soundness, and a verified implementation"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6585633"}},"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":"Q287361$5C59B56C-3478-4D25-9AEF-FE55C898ECD7","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"6d8c2a1cdac6bd606e3b037b3897eb8703bb4a2d","datavalue":{"value":{"text":"Self-formalisation of higher-order logic. Semantics, soundness, and a verified implementation","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q287361$66CC5E50-CD0B-4F9D-B74A-B88C935D4BB2","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"9ed0d4424056e4334bf96b822a0f8531761f92df","datavalue":{"value":"1356.68194","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q287361$886EBD58-1050-479B-8F56-9E9631E11E9E","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"62025305e3524f61b1fc8b1f7bbd2484241846ea","datavalue":{"value":{"entity-type":"item","numeric-id":287359,"id":"Q287359"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287361$1C1C23EF-66BA-4EE8-9F2B-8F40FB3408F4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"a0326155ee2776709b948d74abcb135838e086e1","datavalue":{"value":{"entity-type":"item","numeric-id":287357,"id":"Q287357"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287361$D4EC4AD6-F2A7-44B7-8454-C6319D78586E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"c330e55e5dc72ba4e46dcf35457734e0df28701e","datavalue":{"value":{"entity-type":"item","numeric-id":286789,"id":"Q286789"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287361$94B0C3E4-977B-4F7E-BB03-831A245826DC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"57155b56d8fbcd7c5881cc6580886a49385bb630","datavalue":{"value":{"entity-type":"item","numeric-id":287360,"id":"Q287360"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287361$A24EEBCF-5B7E-40F7-ABE0-E4D3E7144749","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":"Q287361$ED7C5C74-2851-4479-8711-CEDB9CEFE8B5","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"b626bb78b3e93b3076e6958296f7f25e2e74c3ab","datavalue":{"value":{"time":"+2016-05-26T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q287361$C3C94222-D47F-4B8D-B886-20EC8EF4BADB","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q287361$8ED92270-2676-4210-973A-EF00B9ED5C11","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"dd8503cb84d44ac2adb520ebbb11872e6dc1ec3b","datavalue":{"value":"03B15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q287361$919D4593-E22F-4ABD-93B0-3C3FC4E27ED8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q287361$F2E31690-E6AD-4CF3-BE45-548AB18E3E09","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"590319b2a99badffc156dc0076c96ce76ea6c8e9","datavalue":{"value":"6585633","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q287361$870BC574-9D18-4A25-BFEA-2EF85B43140B","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5343ecd15a8e87cb138c7d9e4c8f0d52a5afdb65","datavalue":{"value":"HOL","type":"string"},"datatype":"string"},"type":"statement","id":"Q287361$193EA1F6-24B8-4B6F-BC21-F11D82EDFA97","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"39810ec381ba48fb5861c168391fa7d328efd8b1","datavalue":{"value":"higher-order logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q287361$2285CB37-2A93-4F12-B253-9296243798CD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"66824d9cf653f7dee3c76f98a8ea1aa06432fa7c","datavalue":{"value":"verification","type":"string"},"datatype":"string"},"type":"statement","id":"Q287361$E4A43E7A-2F9F-4A39-8D26-543C8F914D5C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"21cf102e52d55bb9e3ba4ca1c32b8839281988dc","datavalue":{"value":"interactive theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q287361$0D283470-0F6F-4CE6-B632-F1A3F5169D4F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"22498cf86e242a38d9fe355523225aa55193233b","datavalue":{"value":"theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q287361$6981D84E-6E72-45EA-B275-2E84EF42577D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"52c2513afc8941299b07e63a5555cd1e7cb85f4a","datavalue":{"value":"consistency","type":"string"},"datatype":"string"},"type":"statement","id":"Q287361$BF1F9F09-DEBF-4EFA-87B0-C6C1DE735E9B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5d7bfc11de8cab95fd6af201970bd9d16d39bbd0","datavalue":{"value":"semantics","type":"string"},"datatype":"string"},"type":"statement","id":"Q287361$99DB7890-638D-4F0A-8FCF-737346A89BE6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"7ab89ef68ff2cb5e6c29f12a6ca885829d52af42","datavalue":{"value":"self-formalisation","type":"string"},"datatype":"string"},"type":"statement","id":"Q287361$2D4D00EB-50EF-49B1-BABE-317D731D135D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e3b629a0192ce1e5e12a29c32689e4385e2152da","datavalue":{"value":"self-verification","type":"string"},"datatype":"string"},"type":"statement","id":"Q287361$00EB49AA-12D2-40C2-9F17-DE25B0F56638","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"c5fcda2c98ddff866834785339eb37077e5eb1fe","datavalue":{"value":{"entity-type":"item","numeric-id":13212,"id":"Q13212"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287361$12BDED56-5809-4FF3-86AB-289C2111DFD0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"2b02b46847f3d7e3a5825b9484a88607b98dbd14","datavalue":{"value":{"entity-type":"item","numeric-id":13958,"id":"Q13958"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287361$DECC9178-0D91-4BCA-A312-63717CAA5160","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":"Q287361$8A9893C4-8A2A-4DD2-B917-2299DDDFD965","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"25db55153babd7076d594d911b639e78d62b451a","datavalue":{"value":{"entity-type":"item","numeric-id":20369,"id":"Q20369"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287361$0ED58081-22B4-4D17-9DF3-1CE59A0E0126","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"533959f24a509b955614f607e46b8aa4cec190ef","datavalue":{"value":{"entity-type":"item","numeric-id":20799,"id":"Q20799"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287361$3C84AC76-6A59-4790-BD66-8E018C4225F5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"92ada66b7fad67177fdd185887b7c38f3272897d","datavalue":{"value":{"entity-type":"item","numeric-id":40276,"id":"Q40276"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287361$C9F97844-20D3-434E-9C1F-A0387DCF68A1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"801a319db4682ef4442b12d14dec7cb54b5357be","datavalue":{"value":{"entity-type":"item","numeric-id":44336,"id":"Q44336"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287361$079A6B13-1954-4E99-9F2F-47CBDBD581F7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ee80fa482e8c030191fc3263e069d0dc0cdf7815","datavalue":{"value":{"entity-type":"item","numeric-id":18672,"id":"Q18672"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287361$7B6ADB51-F04E-428A-8C96-A4D43059B867","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"2e079f4640d565f0ca1930fd327c2c7e8d634508","datavalue":{"value":{"entity-type":"item","numeric-id":21954,"id":"Q21954"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287361$07F0ADD9-5303-442F-A7D0-40FD85AB6FF0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"44e192ea0614ca90dcab29c306f09db708056c50","datavalue":{"value":{"entity-type":"item","numeric-id":24736,"id":"Q24736"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287361$E5730DBD-868E-4D06-AC4D-D42955443E56","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"c84c15ef2f1b450ae529dcae0c7d808f6b98e405","datavalue":{"value":"Q59476114","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q287361$167C556A-88FD-47D1-A5D1-F7699D5698DB","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":"Q287361$9F707EED-653F-4ABA-9323-1C18505FF9DA","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"4a143f137384f8b4cf2f32bbba62ead81efac1ed","datavalue":{"value":"https://doi.org/10.1007/s10817-015-9357-x","type":"string"},"datatype":"url"},"type":"statement","id":"Q287361$74445C1B-EA77-40B1-91B8-8E2EF1DA7C9F","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"8d282d767ac4a30e3102b8bdb67055f65290c542","datavalue":{"value":"W2339308944","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q287361$159A3CE3-A21C-4A39-A45E-24FCB451212C","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"db7da8d17bd98f8d5a342c642c4fabe6e5f07b9b","datavalue":{"value":{"entity-type":"item","numeric-id":955386,"id":"Q955386"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287361$3865A0E0-E920-460B-82C4-04D14A63D022","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c9864722e1120856743b1e5eb3761fb8bcb430e4","datavalue":{"value":{"entity-type":"item","numeric-id":2879241,"id":"Q2879241"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287361$DC1D785F-4D56-407C-9626-FA05B5983442","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b11646dfc2677d6614fa16128dbbd7844776606d","datavalue":{"value":{"entity-type":"item","numeric-id":1847766,"id":"Q1847766"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287361$B1DF9FF3-5D1B-4454-A058-6D322249F533","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0f77c0a86943e8d93be63fc22f23daf955241422","datavalue":{"value":{"entity-type":"item","numeric-id":2879274,"id":"Q2879274"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287361$E9258B9A-4EF1-4E2A-A40E-A83B480F2986","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"739330a58a3c3aae77075c5fb847ca13d50160d0","datavalue":{"value":{"entity-type":"item","numeric-id":3075242,"id":"Q3075242"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287361$531F4585-0EFA-4E53-B12A-3911D5CE0018","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"dd9ea7887150abfd8958ac46eef7ddf839a8f58f","datavalue":{"value":{"entity-type":"item","numeric-id":3543643,"id":"Q3543643"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287361$0E67119C-12AB-44E5-B1E9-25F60782DB9A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f3a9a03ca7f35c079c210036c3416fa8438e5201","datavalue":{"value":{"entity-type":"item","numeric-id":4513619,"id":"Q4513619"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287361$4AB73749-8739-4E63-BDBE-D2B0D5CA34E0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"aeedc506ee95714a79cfc16f82862182df8774bc","datavalue":{"value":{"entity-type":"item","numeric-id":3613408,"id":"Q3613408"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287361$46B5BC36-BBC0-43D5-B8CC-E3C41D64E2DF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"17a69741364102658aa60a87b94db8d7506ce725","datavalue":{"value":{"entity-type":"item","numeric-id":3183517,"id":"Q3183517"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287361$4901EDC3-2028-42D6-A609-CE6FC8828832","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":"Q287361$2291B65F-D0CB-4988-A17E-B110278BBC63","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5bbf3fd853a4036d3cac2ccc1f0a3b4a11edb981","datavalue":{"value":{"entity-type":"item","numeric-id":2248021,"id":"Q2248021"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287361$DAA28F4D-26FC-4951-BD73-9C7C65E6B49F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"67c913a72527b57ea467866b24b8cfd23fe78226","datavalue":{"value":{"entity-type":"item","numeric-id":5747659,"id":"Q5747659"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287361$153BFEBF-BCBC-4C53-9AAE-1EFDD2985498","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"999b14224255809098a606c16262602638de58e6","datavalue":{"value":{"entity-type":"item","numeric-id":2879260,"id":"Q2879260"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287361$4930FAEF-0467-403D-B7CD-D9DBA4E87EB4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6d1e46bde366c9665559a7c22a84b5c9d3a328b4","datavalue":{"value":{"entity-type":"item","numeric-id":5408415,"id":"Q5408415"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287361$9D02B6CF-40F0-4750-B8DA-10766E75677A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"839fe9e80ad88458f41a8a24be5284fc203e2e80","datavalue":{"value":{"entity-type":"item","numeric-id":606999,"id":"Q606999"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287361$3442DEA3-49E5-4FC6-BAA1-D8C10E49B8C4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6cc440e6b746fbcc870102f7e0b8b66275986778","datavalue":{"value":{"entity-type":"item","numeric-id":5320764,"id":"Q5320764"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287361$064707E1-66BF-401A-8B41-647B5CDCB21B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"436d4ddccf9258c9f31fa193f202f774ffec18b8","datavalue":{"value":{"entity-type":"item","numeric-id":1250704,"id":"Q1250704"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287361$225C28E6-3108-4A59-8EBA-373D9F097511","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ac497f626b608c6620476476c3df0e4c5760d79d","datavalue":{"value":{"entity-type":"item","numeric-id":2879267,"id":"Q2879267"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287361$AC19CAD0-1395-4472-8311-79AC63BAF585","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"227fe77aa9bac83e88e8a7622effb8e94001c51a","datavalue":{"value":{"entity-type":"item","numeric-id":2875232,"id":"Q2875232"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287361$6349F72F-24C8-4866-8782-322E070A1423","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5f4c3f6b3cb1159b66311b6728b700a3178bfb48","datavalue":{"value":{"entity-type":"item","numeric-id":5327372,"id":"Q5327372"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287361$861203F0-DBA4-48C6-85E3-F85A6269123D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"58b883d872eefbd5f8daf82a38b9e66e81e1a15c","datavalue":{"value":{"entity-type":"item","numeric-id":5477663,"id":"Q5477663"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287361$D09EFD40-9565-4F57-881E-6F4CA77BBB1B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"77f4334b25d43b9293350a877e2d317280ca55a9","datavalue":{"value":{"entity-type":"item","numeric-id":3543646,"id":"Q3543646"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287361$9B09E8D8-21E5-490B-B211-F2A66A41D97B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e299933ed7a897a26d196637e2344ecc9a867479","datavalue":{"value":{"entity-type":"item","numeric-id":4326601,"id":"Q4326601"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287361$9072635B-F025-4F28-A19C-4263AB7FC2CD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"efbf9b29f74753ca9de9a61e2d0ebdd560c657a7","datavalue":{"value":{"entity-type":"item","numeric-id":2958550,"id":"Q2958550"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287361$FE5FAB22-4813-41A4-B7E1-A62D1ACB7B10","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"81087b834bd0f0342fd52d99726619dd5c97caec","datavalue":{"value":{"entity-type":"item","numeric-id":3543647,"id":"Q3543647"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287361$61C71422-112A-4085-A25E-CF30D0A61E07","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d15b95442e7c0b28536b0b362e6b88570617db87","datavalue":{"value":{"entity-type":"item","numeric-id":4964711,"id":"Q4964711"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287361$589FEF98-FA50-40B4-8A31-F569B7597AA1","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"285fbe1f82d9dbffa51f12595b016440b0786fdb","datavalue":{"value":"10.1007/S10817-015-9357-X","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q287361$7E730E3B-7D47-4FB7-91EA-DF0F31C2FC7C","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"33d9d91864fd36c9cf69a0a0271de5d035ba5751","datavalue":{"value":{"entity-type":"item","numeric-id":2879260,"id":"Q2879260"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e6a850bc2c5af92fd3b34cde9ca422c071e9a6e1","datavalue":{"value":{"amount":"+0.8948500752449036","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":"Q287361$0070C4B3-457A-468E-A659-365EDFEBF2D0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f1cab783396284eb004b42756f108087b79277b8","datavalue":{"value":{"entity-type":"item","numeric-id":3613408,"id":"Q3613408"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"388f30970a5d9ece28deb4b0ee8cc70abc3242fd","datavalue":{"value":{"amount":"+0.8205186128616333","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":"Q287361$88459D9D-2D7E-4B0F-9FB9-AD11A2A1F828","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"71118114fbb65a0d0338d16dfefbe08e60cecc80","datavalue":{"value":{"entity-type":"item","numeric-id":935562,"id":"Q935562"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2cdcda202e28e38bbbf53c67e29b88c5bcde32a0","datavalue":{"value":{"amount":"+0.7851929068565369","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":"Q287361$122EFBBC-246B-402B-BC4B-6465C2ECDE24","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8a9340227e03cb52d0a7ec16f7ac5a22cc95744b","datavalue":{"value":{"entity-type":"item","numeric-id":5327372,"id":"Q5327372"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"497bbb3c30a0cb94de301ba8aa8ecf70dd8fee05","datavalue":{"value":{"amount":"+0.7771347761154175","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":"Q287361$05F7A94F-7360-43DB-98BB-46988D3E5E4F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"bd58fd6243ca5ecfa61b5100df2e972a1ed7fb82","datavalue":{"value":{"entity-type":"item","numeric-id":5458382,"id":"Q5458382"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5f2b70145392ef6fe9c1a416aa6100c5a7e39b88","datavalue":{"value":{"amount":"+0.7513478398323059","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":"Q287361$35EF12A2-F7C5-45AB-AD86-5A7C29812F23","rank":"normal"}],"P163":[{"mainsnak":{"snaktype":"value","property":"P163","hash":"45fcd4163b5f33e6e8c784f5522d7246c0a1a61e","datavalue":{"value":{"entity-type":"item","numeric-id":57056,"id":"Q57056"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287361$CF6125D0-D713-41E0-AF9D-7994620E4F2D","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Self-formalisation of higher-order logic. Semantics, soundness, and a verified implementation","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Self-formalisation_of_higher-order_logic._Semantics,_soundness,_and_a_verified_implementation"}}}}}