{"entities":{"Q6587256":{"pageid":14198412,"ns":120,"title":"Item:Q6587256","lastrevid":55725676,"modified":"2026-02-17T21:45:16Z","type":"item","id":"Q6587256","labels":{"en":{"language":"en","value":"Verified AIG algorithms in ACL2"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7896675"}},"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":"Q6587256$7083A48E-C5CA-4505-BF1B-67B5388DEC90","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"85594119f62f83a1fa8cc066dcaf199c4e9e7d7d","datavalue":{"value":{"text":"Verified AIG algorithms in ACL2","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q6587256$0DB79DE3-09A2-4C45-A740-A1593B4C2345","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"68abe55ae67918974a7bdca20502a14cf306dd66","datavalue":{"value":"1542.68095","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6587256$7E643A1F-9F4F-4465-8F86-5E29C3846CBE","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"ccf5d4548c5103107f736d99d04459a5f9188db5","datavalue":{"value":{"entity-type":"item","numeric-id":286788,"id":"Q286788"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6587256$E54A5B10-F821-43E6-9C85-667D1B3CA893","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"adc349d912c88af52e08d65ed04aff6f75f7b039","datavalue":{"value":{"entity-type":"item","numeric-id":5747667,"id":"Q5747667"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6587256$D2F47E55-0B77-41A3-BFBA-1FDCECA36E05","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":"Q6587256$171EE427-C4DD-4BFC-8202-E40775F56A32","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6587256$CBE1CDF1-6CA4-4A37-96BA-1B45A4111FFC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"58b3a5d0bc4bfd215423308dfe52b6887acdeedd","datavalue":{"value":"68V20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6587256$1BFA702E-755F-485D-8BBD-04BA30570763","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"e62f6d1638a2bc5e3fc88d4b7c199db27e600be5","datavalue":{"value":"7896675","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6587256$EFFC8101-CD53-47AD-9D75-1BA7B774B79B","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":"Q6587256$19BD9B33-4BC2-47AD-9EBB-BE9F9212FD5D","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"bb15445443b7a8677c7ef043ed8530f20d54b0c3","datavalue":{"value":{"entity-type":"item","numeric-id":3100209,"id":"Q3100209"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6587256$67A63B60-7254-47C8-A346-00CDAF55326F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"efeed698c61c9d4088905eab8917123fdb73bb41","datavalue":{"value":{"entity-type":"item","numeric-id":3100212,"id":"Q3100212"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6587256$B3E9C44C-B80E-46B6-B13C-C46070BFC965","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"fc3406683ad00aa9363d90c4954863b73476c44d","datavalue":{"value":{"entity-type":"item","numeric-id":2843317,"id":"Q2843317"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6587256$2A1DA011-A3F4-4251-B0F8-3B3D63B802E0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f97214e6ee417b23719b1926d0dadcd8c017b900","datavalue":{"value":{"entity-type":"item","numeric-id":3612472,"id":"Q3612472"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6587256$553EC83D-3F80-4F75-A57B-92F81EA510C1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"22485e2e7f5d751287059d6c89f8749b6a408a20","datavalue":{"value":{"entity-type":"item","numeric-id":5325885,"id":"Q5325885"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6587256$E238F5E9-0493-4567-99FE-02064A7EDEC5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"879dcd858f7bcfe1ef3910bf97ce3d345da5b737","datavalue":{"value":{"entity-type":"item","numeric-id":3088019,"id":"Q3088019"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6587256$15B9A544-AF95-456A-92E9-098F56066E95","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6cc8abb92210655a5bd4143cbbadd6eadb52d635","datavalue":{"value":{"entity-type":"item","numeric-id":1801222,"id":"Q1801222"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6587256$8E07A7CD-06F7-463A-90BD-D9C170D8763E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"bd7520de1b4bf1bc0bba49f7075996531473a953","datavalue":{"value":{"entity-type":"item","numeric-id":5477654,"id":"Q5477654"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6587256$7CC1C098-C65B-441F-833E-A57C4B41E2AD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ca81754a5900980091f93b6caed1b08a65835a9e","datavalue":{"value":{"entity-type":"item","numeric-id":5187975,"id":"Q5187975"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6587256$A708D63B-2D1A-4815-805C-09E5BBA2046C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"bd1f0a4023c091ac20c2d3159d071145e434c691","datavalue":{"value":{"entity-type":"item","numeric-id":6586531,"id":"Q6586531"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6587256$E98FA7DF-0415-4F0A-A6CB-05E2A0103560","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ea7fb806cb84b37335d37b3efe1590f8bc64cb5d","datavalue":{"value":{"entity-type":"item","numeric-id":839035,"id":"Q839035"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6587256$2B6CF8C4-B640-4C6B-81FA-7DEE47715F21","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f24266047ac8ffcefe32630c940ffdb70489bec0","datavalue":{"value":{"entity-type":"item","numeric-id":2891429,"id":"Q2891429"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6587256$9CFEFC48-3398-42FD-B68A-92C2180FE8C9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"20f4540009a7df1dd9572f81adbfd34cb4f721c2","datavalue":{"value":{"entity-type":"item","numeric-id":5088165,"id":"Q5088165"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6587256$9683A296-669E-4135-A0BD-F95DF8A024C4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b50deb582ddf6cc285d1ad26fd053f8f3c24878f","datavalue":{"value":{"entity-type":"item","numeric-id":5747668,"id":"Q5747668"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6587256$E8FDC2D9-9169-4BCB-8AEF-70314AE3DB51","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2c6b871d25a3f2bcc10ef5d12d2a6df59054c7c5","datavalue":{"value":{"entity-type":"item","numeric-id":5604434,"id":"Q5604434"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6587256$1B1473CA-9142-435B-BD52-70E0A3D9BCB6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"271326b3f6ba4699b8b9534f6c64338c8ddd3a50","datavalue":{"value":{"entity-type":"item","numeric-id":1006729,"id":"Q1006729"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6587256$40C7DE8E-7482-4659-BDDF-2861EAE1CF1F","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"fbb8b1747ef8901bfea9a06a7103080b479f86b1","datavalue":{"value":"10.4204/EPTCS.114.8","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6587256$D1AE6740-7E96-4B18-AB0B-E7A770786A32","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"06dfee7a404428861ae75e2001b3242657c12349","datavalue":{"value":{"entity-type":"item","numeric-id":5747668,"id":"Q5747668"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a75ebc350aba240e764ffc27124b80d542b471e0","datavalue":{"value":{"amount":"+0.8245306015014648","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":"Q6587256$07F119D4-F2D2-4B08-A751-C179727C33F6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"eaea0953ae6c10369c1f8aacd62d1412843a005a","datavalue":{"value":{"entity-type":"item","numeric-id":3724245,"id":"Q3724245"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0bb77447336272aa19c7f00361dec3a0d93c9bfd","datavalue":{"value":{"amount":"+0.7011902928352356","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":"Q6587256$A059E684-0C7F-4D8F-8B61-04F64C9B6D82","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"760a14bfabc4e10a8a1363a170fc2f2ca225ee11","datavalue":{"value":{"entity-type":"item","numeric-id":3079919,"id":"Q3079919"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ca6d65dcc5da33b599e1e29f66f489205c003819","datavalue":{"value":{"amount":"+0.6961460113525391","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":"Q6587256$3E4EF413-A66D-4A74-B7D0-7FDFCA14F874","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d5ea0b52a3ff78b2c4287a3ca09504684f525ca2","datavalue":{"value":{"entity-type":"item","numeric-id":1312163,"id":"Q1312163"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7e681c88e0712fd5f4bf2f5d8ea41429aebb243e","datavalue":{"value":{"amount":"+0.6849430203437805","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":"Q6587256$F4C22A85-F000-48F7-B93C-2ADE9C0B4E91","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"12a132e4daa2e15bd5dc269ad3507f16b279f28c","datavalue":{"value":{"entity-type":"item","numeric-id":1687744,"id":"Q1687744"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4c72c664dd20e567ceab16685f3d4c0803f66c6f","datavalue":{"value":{"amount":"+0.6845377683639526","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":"Q6587256$91347F09-3F32-4A9D-9D61-30F7F1E4BE59","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:6587256","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:6587256"}}}}}