{"entities":{"Q2945636":{"pageid":2956356,"ns":120,"title":"Item:Q2945636","lastrevid":85388603,"modified":"2026-06-03T07:43:16Z","type":"item","id":"Q2945636","labels":{"en":{"language":"en","value":"A consistent foundation for Isabelle/HOL"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6481867"}},"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":"Q2945636$D0409A03-2D69-4F98-B315-D988095771AF","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"924ab9f6b4e3b609afbe13a5f1fd5d57ea0b94d7","datavalue":{"value":{"text":"A Consistent Foundation for Isabelle/HOL","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2945636$25200D2B-CAF8-4BEB-9885-0D4EBE1BF279","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"bd055d8379fb357c7c58f05d5e2e040480b8e3ec","datavalue":{"value":"1433.68556","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2945636$FDF039EA-7632-4038-9014-6D485F8AFE4A","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"9a47ba6b424cda2aaba0816907fa4899d7128887","datavalue":{"value":"10.1007/978-3-319-22102-1_16","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2945636$85F151F9-B775-42BE-A676-6FBDC765C783","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"cb18cf0542c9d5785b9c3d13ac135abc8a7efb68","datavalue":{"value":{"entity-type":"item","numeric-id":1687532,"id":"Q1687532"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2945636$6D4B81F2-9B9E-4A3B-AA18-A5DCAD5D85DE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"2ef4ea61388b67726824db4b9b444c6863305920","datavalue":{"value":{"entity-type":"item","numeric-id":817686,"id":"Q817686"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2945636$95C98938-E73D-49DF-9C14-EC684482530B","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"d43c6ce6e92d67a2cb7e4a7df2a7d5eeec36e724","datavalue":{"value":{"entity-type":"item","numeric-id":2829237,"id":"Q2829237"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2945636$FB21CE30-990C-4D32-9748-4C0F0B19669B","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"ece460bc202bb4ec344b5d620998e472753b138b","datavalue":{"value":{"time":"+2015-09-14T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2945636$8284EF89-25B0-4417-9814-0C895EE35F98","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"4a506eaca38239289a2480cea5ed3d2ca331c519","datavalue":{"value":"https://eprints.mdx.ac.uk/16073/1/isabelleHOL.pdf","type":"string"},"datatype":"url"},"type":"statement","id":"Q2945636$6382C7C9-B9F0-45C2-B18A-B9D193F629B2","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2945636$89DC934F-364E-4F8F-8415-82D93A9C26E0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"3f6d4b3012578fba2d8ab6b9e39d328cad9def57","datavalue":{"value":"03B16","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2945636$E6E45D66-C5E6-4D8A-94CD-FDA52A1BFEBB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2945636$A7717300-A4E9-4AA9-83D3-2B62F5C0EEF4","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"3d27f9d6e53e4637a9f5fe93ef7b3d33fd51f265","datavalue":{"value":"6481867","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2945636$DA5229C8-A9ED-4236-A57E-B18365646E8F","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":"Q2945636$C06A0B94-AAAA-4A9A-A342-AECF19251259","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":"Q2945636$AB61E8D6-3059-49F7-AC41-551E62196DF0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"1a8b6b13bef47cb19f4e2508b5917af235a65eb0","datavalue":{"value":{"entity-type":"item","numeric-id":21668,"id":"Q21668"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2945636$9956651C-C507-4D1E-AA36-DCAF9E00B621","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":"Q2945636$8BF1757D-C854-4226-AE70-02D16BA28E76","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":"Q2945636$2A17576C-90CC-4CA1-A5FD-31556B769DD3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"8b2040a476017b43b21bd352cfec0a67d631d6d4","datavalue":{"value":{"entity-type":"item","numeric-id":18467,"id":"Q18467"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2945636$9800DEDE-87F8-4487-BED2-3A7BD6C914D6","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":"Q2945636$60AE798C-A3C4-448D-801F-4C126208374F","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":"Q2945636$B871136F-FBB9-4E64-B25E-7F229FFA16E4","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":"Q2945636$541F972C-6BBA-48AA-BCB5-589AAF1F80DD","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"dbf9f96e519ceb61dd4d2823b8672c5d11a5d76a","datavalue":{"value":"W2791394679","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2945636$1F01819F-E656-4C15-9245-374463391902","rank":"normal"}],"P223":[{"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":"Q2945636$253638D1-60DB-40BD-A796-70D903277F76","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":"Q2945636$73EA5A0C-D46F-4262-9E9F-061C6F324DD3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6f3ea02b15a15931f4cd364dd4a0ce61e10ac225","datavalue":{"value":{"entity-type":"item","numeric-id":703860,"id":"Q703860"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2945636$DFA4E8ED-A365-45E0-B52F-DCD1BC0A03AA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"60ec34bc45b3dd9208c19ebd43163fb16d3d98f5","datavalue":{"value":{"entity-type":"item","numeric-id":2981955,"id":"Q2981955"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2945636$E9E5E8DC-8380-4F5B-AF73-6230930A9240","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1903be4a36187a0a0e197e708bc72f62f93b28bd","datavalue":{"value":{"entity-type":"item","numeric-id":3183520,"id":"Q3183520"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2945636$F4DEF91F-EAC9-478C-8ED3-C8D639D7527C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"df6d745c28f41f3f6887e89cc1ca892988e70309","datavalue":{"value":{"entity-type":"item","numeric-id":5287513,"id":"Q5287513"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2945636$AEC90F6B-BC9D-41C5-A669-0B34FFA7DD8D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"14533123e0b9e73c06f9737a070ee002c25f5f1b","datavalue":{"value":{"entity-type":"item","numeric-id":3612442,"id":"Q3612442"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2945636$ED9F16B7-77E2-4D9C-B3C9-C832D285DFB2","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":"Q2945636$A56D444D-B767-4F28-BCE7-FA492BF04878","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8d360f4c10b4163627f57faa3db163275ea6a011","datavalue":{"value":{"entity-type":"item","numeric-id":5327350,"id":"Q5327350"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2945636$A99D0CE2-28D0-403A-A641-1DBC27E6422C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8a7e549f0fba6b332f88c2b3d15bc37b5e90f37a","datavalue":{"value":{"entity-type":"item","numeric-id":5747640,"id":"Q5747640"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2945636$0A308D0B-E42E-46CF-BAAB-03242F895E81","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":"Q2945636$94A1A5D7-B499-477F-8096-C97ED4EB9C84","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5c021bc433feaab99e85a8c56618cc75279c5f49","datavalue":{"value":{"entity-type":"item","numeric-id":2945636,"id":"Q2945636"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2945636$DCDA36A2-93AC-4C19-8AE7-47077336EF44","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a7a1ce015f9a6115f5e15ce96a4b6a73ac4d89f9","datavalue":{"value":{"entity-type":"item","numeric-id":5327340,"id":"Q5327340"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2945636$D11E0C74-F89A-45A2-B2C0-E1612EFC21F2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"923d9841ebb82ba7564626f46c70dd17455ed552","datavalue":{"value":{"entity-type":"item","numeric-id":4267723,"id":"Q4267723"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2945636$7E650242-562E-4F8C-AC30-4676879AF20B","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":"Q2945636$47F744C3-117E-4CE2-8CB2-415FAFBC2840","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":"Q2945636$9FC6446A-E068-4161-A270-812F5241BDA4","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":"Q2945636$75A09344-CBF9-4DA8-8258-42C58A6F372B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"34cc3a3d8722bafd75712de0bd470daeb53e5397","datavalue":{"value":{"entity-type":"item","numeric-id":3527296,"id":"Q3527296"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2945636$A876D4A5-F538-42E8-A2BA-AAFD071D175F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6ff7181965704e473c064c7d95f9f7f0b397f93f","datavalue":{"value":{"entity-type":"item","numeric-id":3543665,"id":"Q3543665"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2945636$E7A29374-BDD7-45A3-8434-0AB0345875D0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4feea37c535bd22cbdd726fd39655db123c9a3f5","datavalue":{"value":{"entity-type":"item","numeric-id":928672,"id":"Q928672"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2945636$BADB625A-4A35-4AAE-8C63-9CFBDF2B6D46","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f007afffaa9d82c697dfde08e38474d46ab399f3","datavalue":{"value":{"entity-type":"item","numeric-id":1739913,"id":"Q1739913"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a21d4c644640581fcad94477a2d2ec1282142137","datavalue":{"value":{"amount":"+0.9992675185203552","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":"Q2945636$86D7C60A-D915-4F22-847E-6316B2663198","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3bab036782718245d05f152a7e71f8f232957e26","datavalue":{"value":{"entity-type":"item","numeric-id":2988665,"id":"Q2988665"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8b4762bd1db3c2e4824689aab96dcd39162eb373","datavalue":{"value":{"amount":"+0.8858530521392822","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":"Q2945636$B3AC47F5-9F23-4AE3-8BB7-93656FA6EF1F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f486f15bb96c9d702825bb4445acddcc63515c3a","datavalue":{"value":{"entity-type":"item","numeric-id":287358,"id":"Q287358"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"76f1178b440149a25f2ecdbfd1c6a0c80802c202","datavalue":{"value":{"amount":"+0.7744643688201904","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":"Q2945636$BEF0CE13-2D42-4C7E-A2A7-90A6D8ACCB7B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6e66700aa57a71e967e8560ef8d8dd1126b71213","datavalue":{"value":{"entity-type":"item","numeric-id":3527296,"id":"Q3527296"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5ca699daa0f3332397fa198a41be1c3daad17812","datavalue":{"value":{"amount":"+0.762473464012146","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":"Q2945636$AAC41A44-CCE0-45AD-8CB0-8D0CB946AC2C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0233b2749ba68d2e1c3ea350d744b8b261347aa3","datavalue":{"value":{"entity-type":"item","numeric-id":2333319,"id":"Q2333319"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5388bf3018e2abf547ad9ec68562a47dfb7bb079","datavalue":{"value":{"amount":"+0.7409958243370056","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":"Q2945636$8C0FFEC8-0086-4F66-825A-1F699CB7C7BE","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"A consistent foundation for Isabelle/HOL (scientific article; zbMATH DE number 6481867)","badges":[]}}}}}