{"entities":{"Q816219":{"pageid":818067,"ns":120,"title":"Item:Q816219","lastrevid":64551603,"modified":"2026-04-11T20:39:34Z","type":"item","id":"Q816219","labels":{"en":{"language":"en","value":"Formalization of fixed-point arithmetic in HOL"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5007762"}},"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":"Q816219$F0544599-6674-4BA9-9007-8C02E3111A10","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"040e78b431619b22a591b1b71b4233cc2a9670d8","datavalue":{"value":{"text":"Formalization of fixed-point arithmetic in HOL","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q816219$FDE8B23E-1D6B-4648-A104-890E0D98830B","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"4888203a04c9ddf99631196171ee0b27a761daed","datavalue":{"value":"1085.68148","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q816219$E6C14FFD-3CD4-476C-B93A-2E66D026E448","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"7f342eecf82498f188d10dbef140d1137265c48e","datavalue":{"value":{"entity-type":"item","numeric-id":816217,"id":"Q816217"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q816219$BEDE9E05-2BA7-453E-9D37-F1383DEDA89E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"f0d2c11253a443ddc53e205509995096ef6b865e","datavalue":{"value":{"entity-type":"item","numeric-id":246141,"id":"Q246141"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q816219$2F126767-EF65-4C5F-8CCD-DA0F1F5D1665","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"2a4e6a34b59f2a5482d2449d845440512b712bca","datavalue":{"value":{"entity-type":"item","numeric-id":816218,"id":"Q816218"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q816219$F5B14DC7-1841-40E5-80A1-0F0C07A2713B","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"70551fcc6e89042fc26ae9242a005533b44a2d7a","datavalue":{"value":{"entity-type":"item","numeric-id":169908,"id":"Q169908"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q816219$7DF7B248-F76F-4AC2-BC5C-97847B5B6C98","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"d5a46ca8715888f9181d63a117c8c9aa412098d3","datavalue":{"value":{"time":"+2006-02-20T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q816219$313DB413-A17E-45D3-B8BB-F20CE6E93924","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"c84e553ca50e3d1a3536c39f099d5a2afdbf4da2","datavalue":{"value":"https://spectrum.library.concordia.ca/977379/1/FMSD-2005.pdf","type":"string"},"datatype":"url"},"type":"statement","id":"Q816219$76776C7A-D218-498D-BC25-075B9FE9D4F3","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q816219$D91A61E6-FD12-4ECD-8EEA-C56A31A7F12F","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"e17fe4334377c0289663c7c645b6b393b0d70ad1","datavalue":{"value":"5007762","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q816219$A6C471D2-0355-41D1-9C44-BB6E30F53654","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c1e5cf016139445db227d3d9c40846221ad303d5","datavalue":{"value":"fixed-point arithmetic","type":"string"},"datatype":"string"},"type":"statement","id":"Q816219$2A3C4A93-8FFB-4ABD-8E30-548FE6795853","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"00216556e27ad3bbc2d642874d0693b52d5f53d1","datavalue":{"value":"floating-point arithmetic","type":"string"},"datatype":"string"},"type":"statement","id":"Q816219$E2BE107F-4DDD-4218-8A70-7044F85CBED4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"22498cf86e242a38d9fe355523225aa55193233b","datavalue":{"value":"theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q816219$6615DBDA-DCCB-4BD2-9016-146F0B5DEF1E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5343ecd15a8e87cb138c7d9e4c8f0d52a5afdb65","datavalue":{"value":"HOL","type":"string"},"datatype":"string"},"type":"statement","id":"Q816219$A620DFDB-1E81-4BE6-8E69-81431C973020","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"02d32efa4caa2abb72a4e6348351cc4a9bcbccbb","datavalue":{"value":{"entity-type":"item","numeric-id":16527,"id":"Q16527"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q816219$E54A0764-D0E7-4C91-B0BA-6F14FF9D788E","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":"Q816219$42B935EE-FD18-40FE-A669-58C8EF72C07C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"2b02b46847f3d7e3a5825b9484a88607b98dbd14","datavalue":{"value":{"entity-type":"item","numeric-id":13958,"id":"Q13958"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q816219$0CC68B54-FBBB-4645-97D0-81D6540B5691","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"6120f2b75e3b962f422b7f4da948411de439246a","datavalue":{"value":{"entity-type":"item","numeric-id":19824,"id":"Q19824"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q816219$3F0C591E-5B30-4E09-879E-39365D90D671","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"8c652637493e8de65377ba80065ca4183c6dc627","datavalue":{"value":{"entity-type":"item","numeric-id":12833,"id":"Q12833"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q816219$F79BABC2-593E-4A1A-A92F-4EAA50F0F7AA","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":"Q816219$C52AC1EA-BA51-473F-97A6-43E8909842E4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"c5a1b3ca07adc1c11c437ea6312362890b614e2c","datavalue":{"value":{"entity-type":"item","numeric-id":37167,"id":"Q37167"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q816219$C90C4E0C-7370-473D-94C5-532B55A40360","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":"Q816219$7E8952EA-CE35-44B9-A4B0-5920303481DC","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"88007022ffd4cc5282aec3170ecc9b3985d4e3b8","datavalue":{"value":"W1967747780","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q816219$BCF5704B-224F-462D-955C-32594DB2299A","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"73be90735838b7922cc6ea358a4a7056c4765ec3","datavalue":{"value":{"entity-type":"item","numeric-id":4787242,"id":"Q4787242"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q816219$352A6D7D-7B2A-4355-B196-42656C766EB9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"91d83abec22f28b19800352199911df73da724ab","datavalue":{"value":{"entity-type":"item","numeric-id":5897057,"id":"Q5897057"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q816219$599FA982-5935-4FF6-8AAC-FD4C5D41D10F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a2940d495eb2b669794d95ca8ddbb03437430e8b","datavalue":{"value":{"entity-type":"item","numeric-id":4790659,"id":"Q4790659"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q816219$43F492D9-4621-4076-96ED-B7A9121E5B3B","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":"Q816219$11BDBDA1-57A2-49A0-B5C3-EBF78D29A461","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"027661121afc8ca039752afc0a4269a02976c160","datavalue":{"value":{"entity-type":"item","numeric-id":1334896,"id":"Q1334896"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q816219$2EBAB71E-21A9-4986-B11E-58ACDB9AECED","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f3c3bf718886c6e11599d9273e2bb7aa3c293801","datavalue":{"value":{"entity-type":"item","numeric-id":2754046,"id":"Q2754046"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q816219$D6EAAB62-16D6-4150-8592-FA2D03B82652","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a6230eb5099e27c7ab57f995d507233f844638ee","datavalue":{"value":{"entity-type":"item","numeric-id":2754053,"id":"Q2754053"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q816219$297E0C85-7641-481F-828F-9CB1F5FAA4F8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2c97813355f8a3ed047649f2193bf1bd050bdd9f","datavalue":{"value":{"entity-type":"item","numeric-id":4494691,"id":"Q4494691"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q816219$6ABC86F9-A3E2-434B-A674-7E427AF457D7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0ec407bff047c5b2a446c4eab8012ded481f5def","datavalue":{"value":{"entity-type":"item","numeric-id":4427909,"id":"Q4427909"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q816219$F64A943E-6E65-46D7-AF84-2737E429A94C","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"72ff0be4522424af962e30db3b5418a9e0561ad9","datavalue":{"value":"10.1007/S10703-005-2256-8","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q816219$36168590-1E66-4650-8B3E-14F78DD4461A","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2136fb2592385d1514bfed4dfbe97047eade54b0","datavalue":{"value":{"entity-type":"item","numeric-id":4737560,"id":"Q4737560"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"26dff4a90665aaa23722cdf711c524b9eb3dff7a","datavalue":{"value":{"amount":"+0.944152534008026","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":"Q816219$AC2616EB-6EBB-4D00-9C56-91D31AB3DDAB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"764c246a1e922833020056c629835fdd29caec98","datavalue":{"value":{"entity-type":"item","numeric-id":5492965,"id":"Q5492965"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5776dcf4564ac0c773c4fbbce3664e0ce3ec89d4","datavalue":{"value":{"amount":"+0.7781316041946411","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":"Q816219$A77C0D2A-F6E5-49D8-8D40-76B9A4C066DE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e9e250971493e7777398b490e966e56ea70e8266","datavalue":{"value":{"entity-type":"item","numeric-id":2520685,"id":"Q2520685"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"74f3cc736f38ddeaee319850d26050e3de788130","datavalue":{"value":{"amount":"+0.776393473148346","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":"Q816219$BCEFBDF1-F398-40B5-A418-35AC68B89168","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3d7e7d6d58357b809f36ec9a1793054a70471024","datavalue":{"value":{"entity-type":"item","numeric-id":6177466,"id":"Q6177466"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"61cb40cb1a23e57f646040653985a119c600950f","datavalue":{"value":{"amount":"+0.7576290369033813","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":"Q816219$92612B54-7D2E-45B3-8A7D-1E23CF1C2832","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ac0ce1a15a6f8a98914f6aa448f055825b864ff2","datavalue":{"value":{"entity-type":"item","numeric-id":714617,"id":"Q714617"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7fb5240fc5660a299b242c2f00905cd44268f278","datavalue":{"value":{"amount":"+0.7468564510345459","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":"Q816219$97F38B25-226C-473C-A5D0-A375B4DAD2B6","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Formalization of fixed-point arithmetic in HOL","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Formalization_of_fixed-point_arithmetic_in_HOL"}}}}}