{"entities":{"Q2351148":{"pageid":2361891,"ns":120,"title":"Item:Q2351148","lastrevid":72576087,"modified":"2026-04-14T05:51:20Z","type":"item","id":"Q2351148","labels":{"en":{"language":"en","value":"Using Isabelle/HOL to verify first-order relativity theory"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6448968"}},"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":"Q2351148$84031CDE-E0AA-4736-BC41-FB66DEBB94DE","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"73d25f2a12856ad8853199a1b415eda88fe33a08","datavalue":{"value":{"text":"Using Isabelle/HOL to verify first-order relativity theory","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2351148$F485C90D-4AB0-4DB0-9D94-24C5BB7764F7","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"6fddcfabfbd1fc5e4bdfd0deca803148958a949f","datavalue":{"value":"1314.68287","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2351148$234E7930-1581-49C2-B9B4-07805DAA633A","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"389bd8189f7428178537e89812ab61524a39750d","datavalue":{"value":{"entity-type":"item","numeric-id":514564,"id":"Q514564"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2351148$FE180C05-B790-4382-8D0F-6915E789EC4D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"857c2c80c4cd84e545d0cc0f92387a21b7c9d079","datavalue":{"value":{"entity-type":"item","numeric-id":227769,"id":"Q227769"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2351148$2B7D4543-65FB-49A9-BA1C-C032289C3AD9","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"b84cc8b5923f45dc86ae69f67f68bf56d7ecfce9","datavalue":{"value":{"entity-type":"item","numeric-id":174771,"id":"Q174771"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2351148$8FB47859-2FE6-4150-88D9-CB751934115F","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"c61f53f8f8d7719eaa1ef54a22f9b50ec39aa46f","datavalue":{"value":{"time":"+2015-06-23T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2351148$6D1D43D1-D512-4F90-B524-AF1625F445F9","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"f21eeb671d3aa0dabc3bec716726d2f315f86e8e","datavalue":{"value":"https://arxiv.org/abs/1211.6468","type":"string"},"datatype":"url"},"type":"statement","id":"Q2351148$74E14814-5AC1-4186-8609-350DECE13E24","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P205","hash":"1098350433c83eb831a7e6c29543984c38eaed3f","datavalue":{"value":"http://eprints.whiterose.ac.uk/76527/7/verispec.pdf","type":"string"},"datatype":"url"},"type":"statement","id":"Q2351148$11D98156-351A-4F89-8281-BC5119E8CDB2","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2351148$9622E7B8-204C-452E-BC7A-9D2E14624B97","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"46a27e96741df7f2155716d2cea6b72fba1257be","datavalue":{"value":"83-04","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2351148$0A5E92B0-9206-4B55-AB2C-A067ABBB49A1","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"b8b06c450f7745fbc4fbf08a78f7ed0ab2c306c8","datavalue":{"value":"6448968","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2351148$AE60CC85-97A7-4BBD-8BEA-1F24289845AE","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ca5830b9e054ca240b1ee150695772e6c0bd6aa7","datavalue":{"value":"\\texttt{Isabelle/HOL}","type":"string"},"datatype":"string"},"type":"statement","id":"Q2351148$1EDCC399-C8F8-4BB6-BF0E-05440F93F582","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e3e91e40d0cc9882cc16e9517a3c41ce2d31365b","datavalue":{"value":"first-order relativity theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q2351148$8E02EF08-501F-4E5E-844B-CE116FD86487","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"41db9a25d7ec51fe95032f4acc75058f2a77e7d3","datavalue":{"value":"hypercomputation","type":"string"},"datatype":"string"},"type":"statement","id":"Q2351148$7AF2C250-6AE3-4AA4-BC93-30C5E2FAE301","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"2b210bfe77585b0bb633df1c957114f2c43391e2","datavalue":{"value":"physics and computation","type":"string"},"datatype":"string"},"type":"statement","id":"Q2351148$F7B6082B-EF41-44F7-A23B-E09C39363A9D","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":"Q2351148$9171DA89-230A-4DCE-BAA6-48ED9A8A9328","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"b222922e2b373ab7fb2b7a049f9de07c755ee255","datavalue":{"value":{"entity-type":"item","numeric-id":16770,"id":"Q16770"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2351148$4DE97C1F-8795-469A-8044-89F003BBBE2A","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":"Q2351148$2451E84E-41E0-42F9-98BD-108609584F24","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"bcaf3b20cd7fd897f2f47a708bad9d4f554cb6fa","datavalue":{"value":{"entity-type":"item","numeric-id":14553,"id":"Q14553"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2351148$69D894EA-DB06-4129-BF79-8681315E1C96","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":"Q2351148$14AB5509-3967-48D3-A70A-6B20EBCF23F3","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"021f8c9779881c77f6dcbedf3a584ef9975034ba","datavalue":{"value":"W2085972255","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2351148$247D4529-5809-4A0F-B680-417BEE74D741","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"07ced0239932b5dfad039172204f778ef92c7a72","datavalue":{"value":"Q57691192","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2351148$56018A73-91B8-447D-A5AF-F41DF166BA1A","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"1460eea28717090fd4093119b50b98c41afdd2e0","datavalue":{"value":{"entity-type":"item","numeric-id":941737,"id":"Q941737"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2351148$463E2C6F-1E3D-467A-A690-CCAC71483F00","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"052dbddc03cea963768ff303a4a85c2a3c02b094","datavalue":{"value":{"entity-type":"item","numeric-id":383001,"id":"Q383001"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2351148$C6FC62E0-823C-4A58-89FA-AC57F5CF127D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1613a6ff5ac7b010de5ba58e55ebd9cdec3d5273","datavalue":{"value":{"entity-type":"item","numeric-id":5765445,"id":"Q5765445"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2351148$973AE804-3519-4FAF-8D0A-FA912FAF689F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1a76fb03a61a86452e14f485a55e91565e9d34bb","datavalue":{"value":{"entity-type":"item","numeric-id":5959223,"id":"Q5959223"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2351148$193A5D05-088D-42C2-9A06-432AF4C9AE0B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"cc8c20b40d808dba8a3572f5a4f70beb17516afa","datavalue":{"value":{"entity-type":"item","numeric-id":4670578,"id":"Q4670578"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2351148$53888863-A384-43DC-BD5D-CD983359EA6A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e54942519755bcf0dafc6d2420e04e9605d723d4","datavalue":{"value":{"entity-type":"item","numeric-id":967229,"id":"Q967229"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2351148$A22890BA-D966-4959-BC2F-ECD2F69A5133","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5cb192c24b740969c370ee112d6efa646c25b6bd","datavalue":{"value":{"entity-type":"item","numeric-id":2842651,"id":"Q2842651"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2351148$BBEE12DA-E979-4FCD-91BE-153823A483E2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8381c7896cefd709e0eeea8bcc9b58835c809207","datavalue":{"value":{"entity-type":"item","numeric-id":2497872,"id":"Q2497872"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2351148$0F44695C-81F0-4163-8C57-E93B1A5BB351","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"41c8a5876988af1c77ae7792ea8c002b3e2c9786","datavalue":{"value":{"entity-type":"item","numeric-id":514581,"id":"Q514581"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2351148$281FC058-E811-4751-A346-65C21BC86BE8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b5bb33faa20f7496ce558584a84a20a5380e2008","datavalue":{"value":{"entity-type":"item","numeric-id":514557,"id":"Q514557"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2351148$811E53BF-C42D-43B4-80CF-F78AE7B43CEB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7e6db2749aed88b70f07c07895ab48caffc2e52b","datavalue":{"value":{"entity-type":"item","numeric-id":4648190,"id":"Q4648190"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2351148$F06C1F9A-369E-4FEC-A699-EAF5765C30CD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8d4997e43efd1b4e8e54b91288b11f37f14ede2b","datavalue":{"value":{"entity-type":"item","numeric-id":2904449,"id":"Q2904449"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2351148$E530A772-8EB8-4ACE-BF16-C4F28B6C358F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a41122bbbde1487e0c13d150fe136888e9e463d7","datavalue":{"value":{"entity-type":"item","numeric-id":2447104,"id":"Q2447104"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2351148$59F15788-C546-4CBF-BBFE-B5E7F86C63AE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"accf79840d0f58d18961b8ab5e205c1309f6538e","datavalue":{"value":{"entity-type":"item","numeric-id":2505242,"id":"Q2505242"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2351148$CBFCD728-AD13-499F-9589-047EC61BDBF5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"13218d45d2f461997ea15755269e247224e547bb","datavalue":{"value":{"entity-type":"item","numeric-id":4913832,"id":"Q4913832"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2351148$933C77A6-40B0-4E26-93C2-A7D4B54BC4B6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"397928bda70fd0e8d92691a953368f289adcc4e9","datavalue":{"value":{"entity-type":"item","numeric-id":2497881,"id":"Q2497881"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2351148$2E174257-A69C-4282-91DC-D7782D447326","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ee98c99de49d1c119a84d4851e107e5c04af6f68","datavalue":{"value":{"entity-type":"item","numeric-id":5898838,"id":"Q5898838"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2351148$DCBBDC22-99D8-47D5-BA26-0DF0712C5EDF","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"303d91b4e8309f2971b594e63364b479d7905944","datavalue":{"value":"10.1007/S10817-013-9292-7","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2351148$EC6EFB27-78C2-4A89-927B-AAFD1A3946F4","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c99890a9c008680117f124c46864667ed8cfb2e3","datavalue":{"value":{"entity-type":"item","numeric-id":514557,"id":"Q514557"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4c2c7019d6e26e19f5c7f62c3767ee4b0c7b5c02","datavalue":{"value":{"amount":"+0.75013267993927","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":"Q2351148$3E37C58A-E5CF-436E-84D6-9971CF424CF9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"659cd151d3c8152fb97efb0bee340318c2c8a221","datavalue":{"value":{"entity-type":"item","numeric-id":3367316,"id":"Q3367316"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"07bc9a8c269cdd255e3efe9673dfd2381a797986","datavalue":{"value":{"amount":"+0.7136377692222595","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":"Q2351148$D9AD001F-6383-4A85-A7DD-F9C8BC79140D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"03f6f054b312b3fc4dcd215df1282395b0342248","datavalue":{"value":{"entity-type":"item","numeric-id":5482812,"id":"Q5482812"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4352bfd1c99d0fb4141fd463a13b21cdca857320","datavalue":{"value":{"amount":"+0.7025447487831116","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":"Q2351148$25667721-9E6F-4C7A-ACE7-DF1760B92BBB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"140576b4d917f46ec7f3bf2c1b3333b3f2b3c316","datavalue":{"value":{"entity-type":"item","numeric-id":5327342,"id":"Q5327342"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"36efcf54d7de6ac707f4db66eaf10896aa86b796","datavalue":{"value":{"amount":"+0.6962284445762634","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":"Q2351148$B5A449A3-1A3D-496A-BC87-015B6D04EE6A","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":"138c2e237dcae0255cda5fabd51b433b318f520f","datavalue":{"value":{"amount":"+0.6955847144126892","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":"Q2351148$5364F0F2-8995-4886-B24B-3B0352E56013","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Using Isabelle/HOL to verify first-order relativity theory","badges":[]}}}}}