{"entities":{"Q4647567":{"pageid":6677148,"ns":120,"title":"Item:Q4647567","lastrevid":53321210,"modified":"2026-01-24T17:45:06Z","type":"item","id":"Q4647567","labels":{"en":{"language":"en","value":"A two-level approach towards lean proof-checking"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7002042"}},"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":"Q4647567$F953AF91-5163-4722-A8AE-2110184869FD","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"782b2e4641c80ccf1f34d6dc008cfcdebf17f03a","datavalue":{"value":{"text":"A two-level approach towards lean proof-checking","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q4647567$C6D974E7-4C87-4723-B395-FBF9B0917B88","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"c4cfa53048b926ce930489c6110d77567bbdbd99","datavalue":{"value":"1407.68431","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4647567$D64465B1-E61C-4064-8D65-818CA9BBD83A","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"d9af7beec87f98100c585c0121b57f8b4fff2771","datavalue":{"value":"10.1007/3-540-61780-9_59","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4647567$861ED56F-D966-443C-B290-A797C456824B","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"df85df02f9f01c867f5b97dc99ba15582bedbdd2","datavalue":{"value":{"entity-type":"item","numeric-id":236461,"id":"Q236461"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647567$2109221D-0A15-4A57-8EFE-5159249B2CD1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"2b0be30d548d17c988631cae31bc7c7884d2c934","datavalue":{"value":{"entity-type":"item","numeric-id":4647566,"id":"Q4647566"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647567$BF88B0F2-2248-40A6-B367-26937D8E4B1E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"77409c9e904108aefa46d70345016e61363f1c7a","datavalue":{"value":{"entity-type":"item","numeric-id":801049,"id":"Q801049"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647567$C4ADA329-DF85-4552-973C-9C99EDC21817","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"85c07c7737819bff773f78e2590a3bb761fe677b","datavalue":{"value":{"entity-type":"item","numeric-id":162374,"id":"Q162374"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647567$B0956057-9E03-4B95-B283-E8FFC73B2F48","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":"Q4647567$3D905BDD-CA14-4360-BA6B-10E2A0050FDE","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"076260f68195f386a7992dd520b4c1eae1038272","datavalue":{"value":"http://hdl.handle.net/2066/17271","type":"string"},"datatype":"url"},"type":"statement","id":"Q4647567$165DFA2E-474B-4795-9C4B-6E40A253F53E","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4647567$29A8471E-DEF6-49B5-ACE1-47AA81CB79FF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4647567$42F1F3E0-1923-4AA3-8D6B-A05D08D4361C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"6be78f1bad1f2f19058dbde65eb124c0430a7d27","datavalue":{"value":"68W30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4647567$09AFA603-3ED7-45C0-AE65-5466A6298897","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"d47cc418bb11679e850c776bac664c7bf3b5860d","datavalue":{"value":"7002042","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4647567$691C3530-E6A2-4375-A4F1-3A96061345B1","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5ea0e35eece84bed33461e424b92d07e45bd0c24","datavalue":{"value":"type theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q4647567$258A4B67-8A5B-4D12-8CFA-CEA83A0C8B34","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d649755d7dec7fe8dd2722580b18ccd4bdd91b89","datavalue":{"value":"equational theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q4647567$5A40DB99-A050-4709-BB66-38FA9344EABB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d17109e875f62271267ba944e1d111a7f52ed69f","datavalue":{"value":"computer algebra system","type":"string"},"datatype":"string"},"type":"statement","id":"Q4647567$81AC6E60-D0CB-456E-ABBE-7673D49512DD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"09a188bc590546995974b55a3f2f84f00e08b2a9","datavalue":{"value":"universal algebra","type":"string"},"datatype":"string"},"type":"statement","id":"Q4647567$3FEAC0D7-E582-4633-95EE-71BC99CD696E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"828b921754f69f303bf26617d04c3b905d50dfb6","datavalue":{"value":"equational problem","type":"string"},"datatype":"string"},"type":"statement","id":"Q4647567$2B128C44-3AA5-4C2D-AAC3-E5B35FE2298A","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":"Q4647567$AF6E8671-7B5B-4E5C-A842-BDF1C02D1D1F","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":"Q4647567$E1F1CFBA-1864-4F56-94FB-99D910B6A43E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"55d1796d289926821ff098bc5ea53615142e836d","datavalue":{"value":{"entity-type":"item","numeric-id":21664,"id":"Q21664"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647567$8B8E75BA-8504-48EB-B229-7028264B2EBD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ab6ee58efeeaa685ac2b8ecf828badcfb673e8c7","datavalue":{"value":{"entity-type":"item","numeric-id":12929,"id":"Q12929"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647567$18B5F206-1204-42A7-B590-242F6245B051","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"05e19126d9e9907924a4600d0a5598afdc2c5f70","datavalue":{"value":{"entity-type":"item","numeric-id":20609,"id":"Q20609"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647567$AC9A752A-ECE8-4B0E-A635-4D50C787ACAB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"485f54a0549a89232924cb0abb443c2fad36af9f","datavalue":{"value":{"entity-type":"item","numeric-id":13300,"id":"Q13300"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647567$EC864BF6-1995-4768-B9FE-2915AC8A55DF","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":"Q4647567$C351586D-0953-4CEE-8C66-926E0BEAD641","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"a9301974fbdbf3896f705a4c8ed840f169a9b63f","datavalue":{"value":{"entity-type":"item","numeric-id":19182,"id":"Q19182"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647567$B77F1159-E877-4F64-944F-28C3EE9261EF","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":"Q4647567$93E78763-5FD6-43D3-8661-A51B6DEBA3EA","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"54cd4181470f50de2102ee932318da8db58aee2a","datavalue":{"value":"W1500329306","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4647567$990C6F5C-3A15-45AF-88F1-6B5D208519B6","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"19121fe5036f2676946186c6f9a088bb5b461d0f","datavalue":{"value":{"entity-type":"item","numeric-id":4227289,"id":"Q4227289"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647567$D62D8300-733C-4CD8-BB7A-92E62B106236","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5f69aa78d91c4421b800f99cb382feb266d80c1d","datavalue":{"value":{"entity-type":"item","numeric-id":4647567,"id":"Q4647567"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647567$2DE90D0F-A1CE-4302-8588-8F2195E200E2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"cbab4acd996db78483779636177b87951d203b1e","datavalue":{"value":{"entity-type":"item","numeric-id":3910579,"id":"Q3910579"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647567$5B8CC1A2-17CB-4090-B546-B380F60EC4CF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6865693541f5bc45c0d517a1263aad887cbf5ca5","datavalue":{"value":{"entity-type":"item","numeric-id":5210799,"id":"Q5210799"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647567$5AB1E1B3-843A-47D0-BF9A-5FD1AA4859CF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"37bc8dae1994f1675072ec162c7c6788e05d8d41","datavalue":{"value":{"entity-type":"item","numeric-id":4296744,"id":"Q4296744"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647567$0420D937-CE65-4A9B-A5E8-C645422A361C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d91a6fc5a255cbadfa617ce94146193166c4f9ed","datavalue":{"value":{"entity-type":"item","numeric-id":4247306,"id":"Q4247306"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647567$CCDB070A-5C45-4D77-8C55-E93F77B3BAB8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3ab5d7b35f67f940445411fa45c1b02bcb40d39f","datavalue":{"value":{"entity-type":"item","numeric-id":3999860,"id":"Q3999860"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647567$BDF86A58-563F-4CE7-9EF0-8A731A345FEC","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5ef6f8cd8718f1d64bdad3d35d2a8750a28f6eb9","datavalue":{"value":{"entity-type":"item","numeric-id":3759967,"id":"Q3759967"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4a2ff6ec62df67a164a70f4f75804f4943fa099c","datavalue":{"value":{"amount":"+0.7268660664558411","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":"Q4647567$6AB726D9-2BAD-4280-B7F0-8AA0DECAD9E8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"27e2e2bc72d672edeffb45ebda5680e68269e395","datavalue":{"value":{"entity-type":"item","numeric-id":1744408,"id":"Q1744408"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1bfc82bb6afba2082158ddde41dabf11e55cba1c","datavalue":{"value":{"amount":"+0.720243513584137","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":"Q4647567$1388814A-BC6B-44DF-8242-59B10ABB419E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1fa5a0802698a0678b8093ca6b34b4f52d547832","datavalue":{"value":{"entity-type":"item","numeric-id":5900725,"id":"Q5900725"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"bcdbd36dd54cbf55acc96fc4f260a75bc83d0df0","datavalue":{"value":{"amount":"+0.7097947001457214","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":"Q4647567$5E2325FB-221F-4A3A-9C2F-37A631E6696B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ae1b97a6f9d5931d17692b9da0d3db3bb3213cf3","datavalue":{"value":{"entity-type":"item","numeric-id":3455771,"id":"Q3455771"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"129953fe6ad9e24ca94f079a14dd7fd83888fce6","datavalue":{"value":{"amount":"+0.7078851461410522","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":"Q4647567$F69C4F54-84E3-4A24-9459-F037057BB03D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1c8281b18217b12593bb5968d148e806fa1d5de2","datavalue":{"value":{"entity-type":"item","numeric-id":3386920,"id":"Q3386920"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"40d56092509283cc356fd654cd4daef06b156958","datavalue":{"value":{"amount":"+0.70003741979599","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":"Q4647567$CE6A3004-7017-418C-A32D-0F20381D103D","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:4647567","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:4647567"}}}}}