{"entities":{"Q6586531":{"pageid":14197687,"ns":120,"title":"Item:Q6586531","lastrevid":55725895,"modified":"2026-02-17T21:45:25Z","type":"item","id":"Q6586531","labels":{"en":{"language":"en","value":"How can I do that with ACL2? Recent enhancements to ACL2"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7895640"}},"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":"Q6586531$74720EF9-4D42-4070-BD50-9917EC030F53","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"b64776db3bdf6b0e40f7d4a18719bc69c84177f4","datavalue":{"value":{"text":"How can I do that with ACL2? Recent enhancements to ACL2","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q6586531$D8C4B7DD-B99B-43DE-A9E5-A38B8FCCBD79","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"1aa2697954abb29a030b488ccbd0bcb0aa636fd7","datavalue":{"value":"1542.68211","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6586531$8A2643CC-535F-4C9C-9F49-B6FB95396EE8","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"9e3287b0211e50d819f8f36e99a7da060d3a3fd0","datavalue":{"value":"10.4204/eptcs.70.4","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6586531$3FEE247C-A235-4ABC-9828-B10711C01247","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"e6bbab2ea230ef82cf7d72bee404dd827d5aaeed","datavalue":{"value":{"entity-type":"item","numeric-id":230814,"id":"Q230814"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6586531$562D9CB5-F1D3-4C7D-9CB6-2015D236F484","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":"Q6586531$D6193983-E585-4729-A350-74B644C1EC1A","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"2ef272fad473aebc084962aae26df5cb18b0f7c3","datavalue":{"value":{"time":"+2024-08-13T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q6586531$7F0D5418-F5E5-4301-BF49-9C2F1CBBC1CF","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6586531$F6E573C9-B909-41AB-B4B7-C1954CB7387A","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"6e7d70d4fe544f5570b5876d7a2347b29f2bb7ef","datavalue":{"value":"7895640","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6586531$D0422F2A-7E67-4F16-BF3E-4F2E231C0584","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":"Q6586531$736756B1-822C-4D8C-A2E2-B25415CDEBDB","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"31644e8fd6661bc349ee66382095029b0048c8dc","datavalue":{"value":{"entity-type":"item","numeric-id":6586529,"id":"Q6586529"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6586531$98710507-9002-42F7-8EBB-7B1D7E1AE915","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b7536e92384e11ec3ce8637ede805331f9e036d8","datavalue":{"value":{"entity-type":"item","numeric-id":3997095,"id":"Q3997095"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6586531$3A17CBC4-9730-4CB8-94A2-39A15D516FD4","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8d8d6f50b498868c2bc7d7cb87e1f53d79cebb2e","datavalue":{"value":{"entity-type":"item","numeric-id":6587250,"id":"Q6587250"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e0482b3cbab812cc623ff3a0b222c16a2dec607a","datavalue":{"value":{"amount":"+0.8682871460914612","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":"Q6586531$9617823E-BA1A-4487-9A3C-ACE640AF101F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3b3b0efa447d2f0bb1d07cfcfcea727ec3cbe250","datavalue":{"value":{"entity-type":"item","numeric-id":2280212,"id":"Q2280212"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f043f28a89fc0883897274083dc8c770419b1493","datavalue":{"value":{"amount":"+0.721144437789917","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":"Q6586531$10E3BA42-E726-449B-9E73-6E8A99AAEB4E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7d9ee78884aa7ec91613795c75b8b27fecc1bfd2","datavalue":{"value":{"entity-type":"item","numeric-id":6589548,"id":"Q6589548"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3d807c64cedaab7e0c442e0ab5ed5d3a1c134cd3","datavalue":{"value":{"amount":"+0.71919184923172","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":"Q6586531$3A11EC46-A3F4-45AC-B627-EE9CCEE7AC28","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":"6bc8d44cbeebb95543ac43ae17f88e3ac33ce75b","datavalue":{"value":{"amount":"+0.7178744077682495","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":"Q6586531$9AE0D2E9-0320-4D27-87EB-20D16743D74A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"34285fc8d4e6a3661405248ff0d17629699e2bad","datavalue":{"value":{"entity-type":"item","numeric-id":6591109,"id":"Q6591109"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"032aa4830d7c4bc33feb27543b747a6638996777","datavalue":{"value":{"amount":"+0.7100656628608704","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":"Q6586531$65F849A7-9FF9-4F23-8B24-E5E759052EE0","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:6586531","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:6586531"}}}}}