{"entities":{"Q5428255":{"pageid":7457829,"ns":120,"title":"Item:Q5428255","lastrevid":50222894,"modified":"2026-01-13T13:53:59Z","type":"item","id":"Q5428255","labels":{"en":{"language":"en","value":"Executing in Common Lisp, Proving in ACL2"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5215395"}},"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":"Q5428255$7614FEC2-70E8-430E-A16B-62830A582116","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"8a52d64535f6755f958ed600d1d27d5eb839163f","datavalue":{"value":{"text":"Executing in Common Lisp, Proving in ACL2","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5428255$CBFDC7A8-5DAD-4F0C-87F1-FD9731A45809","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"41852a31caa5af1a697ba9c5f19aa8205b69c379","datavalue":{"value":"1202.68369","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5428255$0471AD58-CA2F-4D58-BE5A-5C7E5A138BC4","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"e33248d80a73e3024726329650441930781a71e2","datavalue":{"value":"10.1007/978-3-540-73086-6_1","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5428255$B4DD65FD-7AB0-40C4-9564-3F0CF1F2353D","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"a0464ba9139175512ab4dc0cca1466f3330cadf1","datavalue":{"value":{"entity-type":"item","numeric-id":5428253,"id":"Q5428253"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5428255$31CB05EE-60DC-41C2-B2A9-35BA4708C7E6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"962ccc22140a8c8a26cb1ba76269211b5ea9b1db","datavalue":{"value":{"entity-type":"item","numeric-id":1413643,"id":"Q1413643"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5428255$5B062E7E-19CF-4BED-ACF4-8ECAAAF7982D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"2742bc74281e45d5f573cb9dc1b7a4db7f023f65","datavalue":{"value":{"entity-type":"item","numeric-id":1565829,"id":"Q1565829"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5428255$1CD95D09-EEF5-4BED-8FB6-4CF7D072EBDE","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"0fde56500ce7b4c1f33971d2e4b588b592b48421","datavalue":{"value":{"entity-type":"item","numeric-id":5428254,"id":"Q5428254"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5428255$143DB163-D30E-4F8F-B247-565CEBFCBFAD","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"f07a6e02313146619eb76647232125f099011046","datavalue":{"value":{"time":"+2007-11-28T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5428255$D18F8E74-0DEE-4972-AAA2-C90D2C800E7D","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5428255$2320E59A-5F15-48BA-955A-532404866560","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"1a2c3a267d39cc0a240359433e7798b450888646","datavalue":{"value":"55-04","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5428255$797AA9EC-7959-479B-B8F5-75D54389297E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"6be78f1bad1f2f19058dbde65eb124c0430a7d27","datavalue":{"value":"68W30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5428255$97B0FFBF-61DD-402D-B987-7E20A6357CFB","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"270a36919d91227dc381aff3ea37fd20dcfb0510","datavalue":{"value":"5215395","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5428255$372F2BDC-96E3-4278-B2BC-FF95E1E484C7","rank":"normal"}],"P1463":[{"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":"Q5428255$A8978BFC-4AD8-4435-8F2F-C99D64DB5024","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"d9db21642bb525242f0a9c25c65251a61579aa2e","datavalue":{"value":{"entity-type":"item","numeric-id":21159,"id":"Q21159"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5428255$2A774051-B6D9-42CF-A4A0-676C6BD69211","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":"Q5428255$61001963-58E9-4341-8A32-9866A3CA5FD1","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"e4fc301a13d195a725ad73e6830df78ea2b46e7d","datavalue":{"value":"https://doi.org/10.1007/978-3-540-73086-6_1","type":"string"},"datatype":"url"},"type":"statement","id":"Q5428255$C0017CAE-1ED7-4B3E-855F-1A942F1A3632","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"f4562084689266f559f9ad7e1a38ab1a906b2857","datavalue":{"value":"W1496793133","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5428255$12723787-7053-4CF5-81D5-1350E306CB75","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2ab816ca20d777bf64b417cd94a39c25aff51b17","datavalue":{"value":{"entity-type":"item","numeric-id":4817211,"id":"Q4817211"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"fdeb0ed263807e88e0575f1608948fd8a62a3b2e","datavalue":{"value":{"amount":"+0.7979872822761536","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":"Q5428255$2C0B7D4C-F38D-4FE4-82AE-9269EFC62B47","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2e8c3f2564b881ea1b7e4341684c21fb5e3646fc","datavalue":{"value":{"entity-type":"item","numeric-id":3003483,"id":"Q3003483"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"14decf775e22f9b289254cc2ad3f31b9ade7f1ad","datavalue":{"value":{"amount":"+0.7499832510948181","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":"Q5428255$CBF6CF03-CB7E-4598-9E5F-4D0CC49BFD93","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"cf2c48c52bdc7c8427d6f3c28effe97624b0aac1","datavalue":{"value":{"entity-type":"item","numeric-id":2734953,"id":"Q2734953"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2bea294c60f6f27ba1b7f355f17e81a312ce449e","datavalue":{"value":{"amount":"+0.7459946870803833","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":"Q5428255$5302AEAC-5DF3-4D67-9413-D53A16D7EBC2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8a057d646087c1a86968ef69c61f7db8a49a696f","datavalue":{"value":{"entity-type":"item","numeric-id":3088007,"id":"Q3088007"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"81e249220231f7538580e1b1029ebcf42d27ccfe","datavalue":{"value":{"amount":"+0.7427790760993958","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":"Q5428255$C2769FEF-BF78-427C-8EBA-E227281E3AE3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c9b7d04a9ff7a9d025be95e1cfc5750dbf6e966c","datavalue":{"value":{"entity-type":"item","numeric-id":3543644,"id":"Q3543644"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"bf3ddbb19667332645ec79d6efe4a52e9d9477e0","datavalue":{"value":{"amount":"+0.7425171732902527","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":"Q5428255$A1E86F0A-FBAB-4662-84C7-0308D22E1F10","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:5428255","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:5428255"}}}}}