{"entities":{"Q5875431":{"pageid":7904982,"ns":120,"title":"Item:Q5875431","lastrevid":40873683,"modified":"2025-04-12T05:19:32Z","type":"item","id":"Q5875431","labels":{},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7649971"}},"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":"Q5875431$6922841B-463F-416A-BAA4-34C04F198FBC","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"b8e4be225a6094490d6530fbb2f56929f5bbbcf0","datavalue":{"value":{"entity-type":"item","numeric-id":682349,"id":"Q682349"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875431$7CEE1D1C-24C1-4164-85DB-90D9A402A3DB","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"6695abe38664d65c38747de7b5fe54d9caa92dea","datavalue":{"value":{"time":"+2023-02-03T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5875431$22D2686D-3780-4CE1-9599-69C7D386760D","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5875431$6AB38452-2001-4182-8D77-E33CEB8314C4","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"d9fd822456a84081130e409e8a6ad11691e71acd","datavalue":{"value":"7649971","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5875431$3B4094E7-4461-482B-9127-FD167C381E33","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"42f0513e500ea6cb630e73925875c7d53ca8d8e1","datavalue":{"value":"Isabelle/HOL","type":"string"},"datatype":"string"},"type":"statement","id":"Q5875431$A2FB1D4F-9CA2-431E-B673-8DA8564CD36D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"fd2e0b1df3cdcc3827d03e73e9e6f30d480b73fe","datavalue":{"value":"LLVM","type":"string"},"datatype":"string"},"type":"statement","id":"Q5875431$D15F01AA-8632-4098-A770-067498276061","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"938358769b4f58ad078254388a41b1d2ec82e622","datavalue":{"value":"separation logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q5875431$B841A6B3-8AD2-48AE-B039-8C56080C0E2A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d9a4fb32e1337567afbea716ab340afdd02981c9","datavalue":{"value":"verification condition generator","type":"string"},"datatype":"string"},"type":"statement","id":"Q5875431$93863138-29CD-49DF-A7C4-F500CCD2016E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d6bc6768f771e8ae47ba1683cf1d33a808061abb","datavalue":{"value":"code generation","type":"string"},"datatype":"string"},"type":"statement","id":"Q5875431$9DC00C00-483A-4550-8147-6A5B46359980","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"56e7f84524c61979eec661db7577d9112d85d0eb","datavalue":{"value":{"entity-type":"item","numeric-id":33768,"id":"Q33768"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875431$B4A604BE-0905-4CBE-BE76-6B7025438F17","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"f86a777ed9723a1505ce676eeb86cd88f8987a7e","datavalue":{"value":{"entity-type":"item","numeric-id":40262,"id":"Q40262"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875431$A6EBB6E1-C37B-4A14-9A36-B74C82723208","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ed664df4807a1c1480dbcce90c73c0ac4e6b59b6","datavalue":{"value":{"entity-type":"item","numeric-id":24733,"id":"Q24733"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875431$AADE6EBC-8043-4CE4-96E0-241BDC6E9248","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"c2e87d897ce5d80b030b7930ad6e7942edbeeaaf","datavalue":{"value":{"entity-type":"item","numeric-id":24996,"id":"Q24996"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875431$633F276A-6A0E-4D42-B457-3DFD32E26544","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"8693d6594a71b0b5c477ef6fe219a510b51255c5","datavalue":{"value":{"entity-type":"item","numeric-id":25201,"id":"Q25201"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875431$021FAEE2-B1F5-4403-B697-1BF311DE186E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"a3f7f8548c5af1e2ae512d0bcfba5384da7ef3bf","datavalue":{"value":{"entity-type":"item","numeric-id":25228,"id":"Q25228"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875431$AD8CE4B0-7E46-492B-8BA6-AF7D22FBB8E5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"7ee2575b4b00dc5c48fe05a1a87740d06a1036d4","datavalue":{"value":{"entity-type":"item","numeric-id":21498,"id":"Q21498"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875431$864CEA93-BC38-4438-8818-5CC10B434B17","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"c9e521c77db45807815f297bb0abd1f031ff43b1","datavalue":{"value":{"entity-type":"item","numeric-id":39832,"id":"Q39832"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875431$8586F2FE-F2B2-4C09-9034-3B41BB3EAED1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"e338912f65cbd77347bbd512933e55736ef58bd1","datavalue":{"value":{"entity-type":"item","numeric-id":40327,"id":"Q40327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875431$3FC31B51-F186-4DD4-89D3-14186FE796F0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"fa5dc13872ba1592e71dabc4befba1daea72a8a3","datavalue":{"value":{"entity-type":"item","numeric-id":14275,"id":"Q14275"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875431$7D399117-62DC-4C00-8F93-BBB3F45C6A31","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"141f26f927e60d71f5bcfefad996453f4c9a6038","datavalue":{"value":{"entity-type":"item","numeric-id":26493,"id":"Q26493"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875431$288A035F-B5E8-4B2E-9A17-7B6343C1FC14","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"8bf42d0fd66acf369e3d5d44d7ebef6adc7ae452","datavalue":{"value":{"entity-type":"item","numeric-id":56651,"id":"Q56651"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875431$63F6D538-65B2-4F3E-BC0F-2C885483FA34","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":"Q5875431$0DB80C3F-5060-469D-921E-20E274A311D2","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"c46319975d5f428b28cf95457785c347fec2d0df","datavalue":{"value":{"entity-type":"item","numeric-id":5494381,"id":"Q5494381"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875431$BB1E2C11-F3A3-4644-AF19-84A0FCF761AE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2f6a505c48f7ed8fbc36053c87307f799e1a7f54","datavalue":{"value":{"entity-type":"item","numeric-id":2351158,"id":"Q2351158"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875431$9B603B87-72B1-496E-975B-C3E7C329D00F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9f90f9000203b5cc02cd5a95785f3228e4b1b7c0","datavalue":{"value":{"entity-type":"item","numeric-id":2655325,"id":"Q2655325"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875431$DF42AF92-2649-436F-9F2A-90F9E9190581","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"76b9c6c60f3db2907a04f9c3b63c103f4fca17c6","datavalue":{"value":{"entity-type":"item","numeric-id":682350,"id":"Q682350"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875431$B7D1D6AF-C7A7-48B4-9CA2-AA8640E6FC16","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e5a1ce762817aa67ba84d34579fd3b9060a2c653","datavalue":{"value":{"entity-type":"item","numeric-id":3543655,"id":"Q3543655"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875431$484D64FD-8BD0-4EF0-B3B5-A14AAFC25B4A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"77bf0527cae45caf1270972ff5ead3c89685a7ab","datavalue":{"value":{"entity-type":"item","numeric-id":5875431,"id":"Q5875431"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875431$30D17EDE-78D1-4987-8E29-F9C04755989D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"086fdbd21f473c213329b475c94f7dc23f61bf59","datavalue":{"value":{"entity-type":"item","numeric-id":1663238,"id":"Q1663238"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875431$F9AAB42C-2D15-4E0D-AE54-6EE3DAA0623B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f4d5ccea7b6fe9f5a7082344f9edaface083da76","datavalue":{"value":{"entity-type":"item","numeric-id":2405252,"id":"Q2405252"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875431$FEB77002-45B5-4100-B414-D87BD242FC71","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"da0d795517e293a55fbffeee6d84c637293c8bf8","datavalue":{"value":{"entity-type":"item","numeric-id":5327339,"id":"Q5327339"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875431$D6D63CD1-C6D8-4C4D-8BCD-9CF98826C200","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8d43182de98d159f0ebb543c5126e0ae385036ba","datavalue":{"value":{"entity-type":"item","numeric-id":1687744,"id":"Q1687744"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875431$55F1C958-8145-423E-913C-FAEE0CED020F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"78757e9c4e37a9fa53a10705a27e9c8cff416b63","datavalue":{"value":{"entity-type":"item","numeric-id":2324018,"id":"Q2324018"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875431$457A6B34-E9A9-4538-A997-154F238D8A1B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"88fbfcea2166cf55628dc74bb062db5b5b011195","datavalue":{"value":{"entity-type":"item","numeric-id":2914753,"id":"Q2914753"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875431$5159F170-093D-4626-A3AD-760AD28EE784","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"cac7f741f9b1e3426d597355d63b43bdf762c36a","datavalue":{"value":{"entity-type":"item","numeric-id":4148937,"id":"Q4148937"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875431$9AEBA52B-A66C-4E09-96C8-E5DE0F25C59C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"50b0bfaa5604fbbf1607bb7e54efdd2fee887b49","datavalue":{"value":{"entity-type":"item","numeric-id":5327338,"id":"Q5327338"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875431$93E37319-69EF-4223-ACEC-A1E31F3334AC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b5dffe5441220fd05c9ab29a095f510d384d606b","datavalue":{"value":{"entity-type":"item","numeric-id":2945637,"id":"Q2945637"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875431$CA0DA3A1-D7DE-42EE-AD92-AC9D4E7C222D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6e4aed9b8c360dba198361b37afc63de7b6c5158","datavalue":{"value":{"entity-type":"item","numeric-id":5920089,"id":"Q5920089"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875431$6BC9BFD2-D4CA-4548-869B-DF13E23F14A1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a6cf0d02217708d84dcdcc681838d7558a420590","datavalue":{"value":{"entity-type":"item","numeric-id":2829260,"id":"Q2829260"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875431$794F16BD-DFD1-4F6D-B1A8-077180C2851B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e18191e110a0c07df939fcb4a6ab2ce398f0616b","datavalue":{"value":{"entity-type":"item","numeric-id":1722647,"id":"Q1722647"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875431$BA360736-556D-4E4D-B506-3B9EB036B2A3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a7f766bae7bb1dc745731294a8b2405f79150a41","datavalue":{"value":{"entity-type":"item","numeric-id":2914741,"id":"Q2914741"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875431$70BED429-A1BB-4F1C-9909-AE05E5189D78","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3465854ebec2bf54cbf9f18bb6fced291b245abc","datavalue":{"value":{"entity-type":"item","numeric-id":2892748,"id":"Q2892748"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875431$44C9CC86-0C96-4B42-BAC5-B3211BBE8772","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"cd1db7dcd2da9fc394dcd951ad62461c4f9bd451","datavalue":{"value":{"entity-type":"item","numeric-id":1227632,"id":"Q1227632"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875431$95914FB6-6668-4FD7-837D-F94F6E22903A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2d8a6a7f4a099b96912e5cba667c8ca70d007bb8","datavalue":{"value":{"entity-type":"item","numeric-id":287365,"id":"Q287365"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875431$39F1BCDE-EFFA-4AE4-9D4C-6B44F64BFC2D","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":"Q5875431$79420220-9386-4197-B9E0-08E60D608770","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7e264974062f53b439460b85662778a60b49509d","datavalue":{"value":{"entity-type":"item","numeric-id":2926333,"id":"Q2926333"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875431$B5CBBC09-D9CB-4A4F-BFDA-5C9B310A9E74","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"84afe353d96a988928bd5d41e96afba7e81d6980","datavalue":{"value":{"entity-type":"item","numeric-id":1600086,"id":"Q1600086"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875431$FD1DB8A2-83A0-4014-A029-9EF55063443F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"cb081c24d3f308759ffc5be25d93bb06a52b464f","datavalue":{"value":{"entity-type":"item","numeric-id":3192088,"id":"Q3192088"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875431$AC2593DB-6DCF-4D5A-B095-C0DF247CCF02","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7abc4c653f1a49315933e87e0214c05e6687fccf","datavalue":{"value":{"entity-type":"item","numeric-id":2324206,"id":"Q2324206"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875431$CEDF9935-C7F9-4998-9E65-05FA8BC9A442","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"40c4d40b22666ac31f4eb490193ee881d1816bbe","datavalue":{"value":{"entity-type":"item","numeric-id":2942893,"id":"Q2942893"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875431$E63AEEF1-4276-4AC7-9257-C55B6272CCA9","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"bacaa2a2863beab79d167b95fe37a54defe57653","datavalue":{"value":"10.4230/LIPICS.ITP.2019.22","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5875431$20797D52-F476-47E7-8CCF-D309B10512BD","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:5875431","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:5875431"}}}}}