{"entities":{"Q2945576":{"pageid":2956296,"ns":120,"title":"Item:Q2945576","lastrevid":52344149,"modified":"2026-01-22T09:46:49Z","type":"item","id":"Q2945576","labels":{"en":{"language":"en","value":"Formalisation vs. understanding. A case study in Isabelle"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6481817"}},"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":"Q2945576$2692966B-C125-44D8-ADB5-F0D3FB807409","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"aaec19445e21ac6bda1221aec99cf468abce9bff","datavalue":{"value":{"text":"Formalisation vs. Understanding","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2945576$1ADA68DB-823F-4214-85CE-C83D80C41A99","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"53a91ff40b24e26b7799aad94cff068b06d7b6c1","datavalue":{"value":"1465.68306","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2945576$C3CFF552-137F-457B-8CA7-30FBFBAC3B3D","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"f80891adc5c4e6c117023ef1cc2fc9e25702f697","datavalue":{"value":"10.1007/978-3-319-21819-9_22","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2945576$5D84D5FC-9E97-4474-9E8B-7A7B603B74E0","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"a17a15ee3958a618cb8b1608e10dde48f4ce52f9","datavalue":{"value":{"entity-type":"item","numeric-id":2148795,"id":"Q2148795"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2945576$5750B8B4-1939-4B5F-A2F2-0E8A8BCEC5B8","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"619541537a393918353c6a64fdcde0dad2978e85","datavalue":{"value":{"entity-type":"item","numeric-id":2819132,"id":"Q2819132"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2945576$CA3053CC-ABF5-47EF-A901-1E5A9C2AA451","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":"Q2945576$3DBB9B59-5B20-4F96-8F67-9B29B4B0B291","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"58b3a5d0bc4bfd215423308dfe52b6887acdeedd","datavalue":{"value":"68V20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2945576$BEC71E97-6613-48EC-8A53-302A4B01AE02","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2945576$04ABCC8A-DED1-4920-9EBF-E99233FF9CD0","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"eda257ad07b63bed607b8021b7c9921b82279c13","datavalue":{"value":"6481817","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2945576$727E4600-94C4-4ECE-BDBE-C2F3CDF3C51D","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":"Q2945576$DB486BA2-1BF0-49D2-AAB3-59DEED2C6DE7","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":"Q2945576$962B7E69-C960-4DEA-9250-D65B0FF86686","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"8ff1fd05d25d51037d0b532207f48b1d74954567","datavalue":{"value":"https://doi.org/10.1007/978-3-319-21819-9_22","type":"string"},"datatype":"url"},"type":"statement","id":"Q2945576$3C49FF34-C403-414F-8300-D600A61A7799","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"00236d9039bd2cacdbf3f7bc0c2a3ff2502cc250","datavalue":{"value":"W2435505789","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2945576$B3EB4D7B-77E1-40B8-8B90-FE9FDCAB1560","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"527bb67f65c65ab8e2b8362b1aec972df57041c9","datavalue":{"value":{"entity-type":"item","numeric-id":3637280,"id":"Q3637280"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2945576$9C457E01-5253-4429-924F-6E561E38A58B","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":"Q2945576$3DE8B9E9-5D35-48A5-8A5C-D2E2956B266B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7c02baa06229f9c8e47415ba00fdd6dfa7fc577b","datavalue":{"value":{"entity-type":"item","numeric-id":5327342,"id":"Q5327342"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2945576$E07AC68D-7F00-4962-9BB8-011E8BE60075","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"284ce6a66d7f458841a6738a24e438a5a5cc3c93","datavalue":{"value":{"entity-type":"item","numeric-id":2829997,"id":"Q2829997"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3d7e688f431f55db6351a9b084d1956637f31d38","datavalue":{"value":{"amount":"+0.7787553071975708","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":"Q2945576$346F46BF-509F-45BF-9936-246998B70952","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"060565dc962325d9cae604367018fca0b1002877","datavalue":{"value":{"entity-type":"item","numeric-id":2657827,"id":"Q2657827"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"041da0693a1b28db81bba8f11407564a18cf808a","datavalue":{"value":{"amount":"+0.7751862406730652","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":"Q2945576$56738DAE-86EA-4593-BC7D-E19F55E1E698","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"bfea782e8ccf212788d53c8f4e477999d4fbba88","datavalue":{"value":{"entity-type":"item","numeric-id":3637280,"id":"Q3637280"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3b55f063d8b61c26d71eaa7ce90b7de118a0b4e3","datavalue":{"value":{"amount":"+0.7629995942115784","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":"Q2945576$4D53E717-7532-405F-8C0E-22B4C894EF4C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"34f4aae526e20b9309e6af8e88049bbed25ec267","datavalue":{"value":{"entity-type":"item","numeric-id":286772,"id":"Q286772"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"07eeea6aec35017778a7168c21416655465d3509","datavalue":{"value":{"amount":"+0.7609549164772034","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":"Q2945576$1A65BCE4-5CB6-42AD-8AC1-FBBAC944829A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2454600514756771921ca2d58e70225397847431","datavalue":{"value":{"entity-type":"item","numeric-id":2940885,"id":"Q2940885"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"10a099c943b28ee6a4973e629ef348619e25211c","datavalue":{"value":{"amount":"+0.7573990225791931","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":"Q2945576$15E407D1-803F-4590-937C-2C999F715CAD","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:2945576","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:2945576"}}}}}