{"entities":{"Q5897076":{"pageid":7937685,"ns":120,"title":"Item:Q5897076","lastrevid":55908184,"modified":"2026-02-21T01:25:08Z","type":"item","id":"Q5897076","labels":{"en":{"language":"en","value":"Linear and nonlinear arithmetic in ACL2"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5667315"}},"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":"Q5897076$4EDD0697-BE54-4957-8127-ED7D22E3DD58","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"b8c8f2d2ec76da52bc4ad5fba0da16b149a776d5","datavalue":{"value":{"text":"Correct Hardware Design and Verification Methods","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5897076$F80D49D1-1022-4715-9E64-3B0C503B2CA4","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"840b509d6f4ce0b528707a06a50700dec74e6d06","datavalue":{"value":"1179.68136","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5897076$816AB834-2393-412A-9AD5-B6629FEFD38D","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"c816a025bc6f755e450b819056444c0dbde28149","datavalue":{"value":{"entity-type":"item","numeric-id":1327710,"id":"Q1327710"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5897076$D602F467-6766-4160-B085-F6C04DBDCD21","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"11673dfb86b4951e4e91e0cb3ab89f54b3e4fd90","datavalue":{"value":{"entity-type":"item","numeric-id":2802934,"id":"Q2802934"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5897076$D1771204-4F29-42AB-BF27-8CEC06A912AC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"b0d384413a2d1b8185eb46b74e5b2c74244e0aac","datavalue":{"value":{"entity-type":"item","numeric-id":928667,"id":"Q928667"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5897076$5829A6FF-D5C3-4B85-9D03-4C356D25A04B","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"85c07c7737819bff773f78e2590a3bb761fe677b","datavalue":{"value":{"entity-type":"item","numeric-id":162374,"id":"Q162374"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5897076$37CF65F8-9B3A-45DA-9551-455AE3C02E45","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"922e941384ccd68eb1997024165e5bf5ef775623","datavalue":{"value":{"time":"+2010-02-05T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5897076$38F26AF4-4571-4245-99AB-3BC4901E8F5C","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5897076$A0D01823-D454-4B24-A161-70A6BD6DDF5D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5897076$774EBE09-981F-4E54-810B-15271A88936A","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"435fce70e27928ae8ddb618c66248d80a66e7e00","datavalue":{"value":"5667315","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5897076$0B34A1CF-B70E-4FB7-9C3D-54EF72DD56A4","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":"Q5897076$9541DE83-05C3-4195-97C3-B0E117E490C5","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":"Q5897076$754BC589-1694-4E70-8AE5-69F161C50995","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"1b8c5cde1231ec6becb5c8cd63c3722e801c9211","datavalue":{"value":"https://doi.org/10.1007/b93958","type":"string"},"datatype":"url"},"type":"statement","id":"Q5897076$7AD6165D-6B3B-4970-B8E7-4ED85BF44AA6","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"652751e9bf248790b4e9b94adeaafb8d6cf26dda","datavalue":{"value":"W219731125","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5897076$153BE434-52EC-4251-8383-15262B4A4B75","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"6fcbd4de8d7777e47679b10069f6a3080aceb1e6","datavalue":{"value":"10.1007/B93958","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5897076$75B32D19-D1E7-4965-AB2E-D63591C4902C","rank":"normal"}],"P1643":[{"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":"8508795553208682240659dc53e74dcc4beb548b","datavalue":{"value":{"amount":"+0.7550998330116272","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":"Q5897076$B30CAF9E-44B6-464C-B78F-70A6E469DD74","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b7fb1101926584588629995559670ee57c402e54","datavalue":{"value":{"entity-type":"item","numeric-id":2642461,"id":"Q2642461"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ac0a5a9b6bc6cbaecffda8ab60ba6cc0d3af9a07","datavalue":{"value":{"amount":"+0.7511783838272095","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":"Q5897076$F2E2D714-8179-476F-A047-6E3449ACE52D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"312b24bd6960c5907e5df9922eecba0ddd49ed2e","datavalue":{"value":{"entity-type":"item","numeric-id":5956117,"id":"Q5956117"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f37f1e6e538b2de788f813c06b736e1da7406b12","datavalue":{"value":{"amount":"+0.7492256164550781","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":"Q5897076$83CB4549-B7AC-4CE0-9B73-433F8FC92D0C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7de94fdb67b3ec18a4a9afac48a95b409770048b","datavalue":{"value":{"entity-type":"item","numeric-id":2908506,"id":"Q2908506"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f199bf7558dd7988f60e68b04bec6664a325bc80","datavalue":{"value":{"amount":"+0.746084451675415","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":"Q5897076$194595CD-F4B3-447B-8E45-EEE6BB2462E3","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:5897076","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:5897076"}}}}}