{"entities":{"Q2879247":{"pageid":2889967,"ns":120,"title":"Item:Q2879247","lastrevid":52085342,"modified":"2026-01-20T22:02:48Z","type":"item","id":"Q2879247","labels":{"en":{"language":"en","value":"Cardinals in Isabelle/HOL"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6341477"}},"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":"Q2879247$1ED23617-5FB6-486D-B448-6AE1870B41CA","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"af5e359aec6709cbf5f33199326ffdd1130111f2","datavalue":{"value":{"text":"Cardinals in Isabelle/HOL","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2879247$58A7A001-0442-4166-A8F5-CB7B68A0B042","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"147b747b41b654ccb80136ba93b880552a48ea8a","datavalue":{"value":"1416.68152","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2879247$ED364F5B-41A4-45AD-A4D5-2B82E13A4A3A","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"69e19c5e520b945cfd6f788c124a95c66af23830","datavalue":{"value":"10.1007/978-3-319-08970-6_8","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2879247$0F968603-F1F9-4F79-8901-8A983A77C9D1","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"42c29c686dffd678d9f155b05a4a1aa93e85953c","datavalue":{"value":{"entity-type":"item","numeric-id":287335,"id":"Q287335"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2879247$A27F0564-9C80-4479-AF99-69217EC6897A","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":"Q2879247$4026340E-41F0-4862-B31F-F8E91DB11431","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"157dc0abe360dacc915db0769a2ed352a42201ad","datavalue":{"value":{"entity-type":"item","numeric-id":1687534,"id":"Q1687534"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2879247$E01DB181-6E1C-43B3-B8EE-713837BE17D3","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":"Q2879247$251299CE-3B52-479B-9620-81485725F310","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"565bc5987614f46e32dc98add32d630fe2eeb533","datavalue":{"value":{"time":"+2014-09-08T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2879247$8C24BCBB-C3B2-40C8-9329-A46B6D86AAE2","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"6fc02a4b3f58757dae828e8956a1f70d6358543a","datavalue":{"value":"https://eprints.mdx.ac.uk/15164/2/card.pdf","type":"string"},"datatype":"url"},"type":"statement","id":"Q2879247$93AEE294-6179-40D7-934A-7B3FCEE14EA1","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2879247$78C00E53-5F3A-4740-86E4-A69A4D0E6583","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"ca56587cb7d44a0a9a2fcf0256e870acd82016f2","datavalue":{"value":"6341477","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2879247$7B424C40-DAE6-4741-AB62-C5D6DDBD9E5B","rank":"normal"}],"P1463":[{"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":"Q2879247$BC2E5DA9-AD08-4791-8A25-68BA8CCE6F15","rank":"normal"},{"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":"Q2879247$39B1A78D-C15E-47C9-8D93-290F1995103D","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":"Q2879247$B3558684-879A-4102-B64B-7531EEF9C0D9","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":"Q2879247$BED201CC-EAE3-442B-8DE8-651F2B3E5295","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"1e52e81783148906b56ed4288705808580f90e69","datavalue":{"value":{"entity-type":"item","numeric-id":40625,"id":"Q40625"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2879247$876B179A-A16F-423C-9D47-B38273907A58","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"930b650ce9c2742a8a6dd4b00a184bf9a4342d24","datavalue":{"value":{"entity-type":"item","numeric-id":40626,"id":"Q40626"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2879247$CB337B46-60B5-4597-9D36-001CCDD2524E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"95458f821e347cc622eedce2f9bdb94b32073280","datavalue":{"value":{"entity-type":"item","numeric-id":40627,"id":"Q40627"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2879247$50B42157-F8F0-4F67-97B9-B238B97DE8A8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"574e03c18db656572f7176b4bc572532542e20cb","datavalue":{"value":{"entity-type":"item","numeric-id":40628,"id":"Q40628"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2879247$5A201E49-8EA5-4420-8001-343D7D17A09F","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":"Q2879247$40F09519-ACF1-4BF9-9788-9A08C039D96B","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"2434f4d08abf517df7aaa14e630527f0f9d504a3","datavalue":{"value":"W1821411012","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2879247$514FDDA8-5A32-437C-A8DC-7891778231CF","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"67817ded466701f9bbe95b0240a3a1e5b5ec9fbc","datavalue":{"value":{"entity-type":"item","numeric-id":5327341,"id":"Q5327341"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"195bdc50afa38d77574ba471e93916abbf06dfa3","datavalue":{"value":{"amount":"+0.7632922530174255","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":"Q2879247$3A7B1358-B8DD-4E35-B438-DE8926CDCC11","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e0a6a39618f02d3d28a619324f6c08ad6f63129b","datavalue":{"value":{"entity-type":"item","numeric-id":5094473,"id":"Q5094473"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f640778398b5ee417ba18839ecc6993de08519d2","datavalue":{"value":{"amount":"+0.7621093392372131","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":"Q2879247$2FD0CD3A-7F5F-476D-A162-A0EC861AB908","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f6946cd334a576097a16d5346c4ccb4db32e8d67","datavalue":{"value":{"entity-type":"item","numeric-id":5961491,"id":"Q5961491"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d0a7fbe6d3ab70778b03b03119bdd30822598477","datavalue":{"value":{"amount":"+0.7458102107048035","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":"Q2879247$E7DEEA25-16CE-4871-B115-00AC9CA25553","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"10712b80cd7952b3c9a1b6eb094b1a55922e0e6a","datavalue":{"value":{"entity-type":"item","numeric-id":5111307,"id":"Q5111307"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9cbcc5923cfdc8fb1c0dde7a26c88e5f17630d23","datavalue":{"value":{"amount":"+0.719631016254425","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":"Q2879247$5BEAFB47-E2F1-4183-8A9D-38E4BC05F934","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"61219fe80357e118ca1092f6e290195ffb650316","datavalue":{"value":{"entity-type":"item","numeric-id":5094474,"id":"Q5094474"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"bcfd3e6a374bbc47c64df14fbb0e4e533bd9f588","datavalue":{"value":{"amount":"+0.7105757594108582","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":"Q2879247$5AA77034-CE2F-4D3B-9D58-3DE7445701A8","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:2879247","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:2879247"}}}}}