{"entities":{"Q2867932":{"pageid":2878652,"ns":120,"title":"Item:Q2867932","lastrevid":51894926,"modified":"2026-01-20T12:05:22Z","type":"item","id":"Q2867932","labels":{"en":{"language":"en","value":"ACL2s: ``the ACL2 sedan''"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6241755"}},"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":"Q2867932$DE8B2D8D-787E-42AF-81C6-78D3DC56ECAC","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"a4c3fe8ff048fa2b35710940f171800745d95902","datavalue":{"value":"1278.68258","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2867932$0F24FA6F-3A7F-4136-B854-494336D10025","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"f3524b9c32b1166213486322dd60fbb6b441c057","datavalue":{"value":{"entity-type":"item","numeric-id":2867931,"id":"Q2867931"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2867932$A5B282A3-5322-4A44-9C9E-59FA87C66B9B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"07ef5bce62b88cfecff16603e8667fcc383b0d99","datavalue":{"value":{"entity-type":"item","numeric-id":479822,"id":"Q479822"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2867932$82913895-D3B4-44EF-BEDE-A0460BBB7CEB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"49a02d2967366c05338e9a85c6a94315b1ebf4a5","datavalue":{"value":{"entity-type":"item","numeric-id":851143,"id":"Q851143"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2867932$7C300E85-07EE-4B0F-8264-34E28A4752C7","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":"Q2867932$43AA85A5-E9FB-4C01-899B-6B17A8E37805","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"3478ec308a15597e43cb648673c843463f4d3028","datavalue":{"value":{"entity-type":"item","numeric-id":163528,"id":"Q163528"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2867932$74ADAA5C-2A6C-4FA4-9A18-9E4CF2435978","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"910ae69968b0b824ffb07e2bd5cc35370f9e2a13","datavalue":{"value":{"time":"+2013-12-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":"Q2867932$842CC903-524E-42CA-B3E8-77C58B999C5A","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2867932$0218C011-A108-426C-BB8F-4F701238B035","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"e1080922a418c87b2f0cd88947cf66bd08687099","datavalue":{"value":"6241755","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2867932$7517C20C-96A5-4917-B080-0509FC4DDF2B","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"24dd5926fa2c4f0ee181b086899e10f05b3e9148","datavalue":{"value":"ACL2","type":"string"},"datatype":"string"},"type":"statement","id":"Q2867932$1C9BB6C8-5B8C-47E1-BBA1-F7D63E3CD079","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"0b5b609580845c3fde78254e089faf0e4f2c160f","datavalue":{"value":"Eclipse","type":"string"},"datatype":"string"},"type":"statement","id":"Q2867932$8D5AEAFA-32F8-403C-AFE5-9EC604B656D0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"22498cf86e242a38d9fe355523225aa55193233b","datavalue":{"value":"theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q2867932$026E7891-FBA4-4405-8E2C-8933EF4483C1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"01c29905c4d6203b1c2be6e3d87ebe0d1b1148a1","datavalue":{"value":"script management","type":"string"},"datatype":"string"},"type":"statement","id":"Q2867932$37E1C6F8-84F0-4465-BBD7-4D35757141A3","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"e8455808aed9282ae1eed82512c469b84dfb04d0","datavalue":{"value":{"entity-type":"item","numeric-id":41360,"id":"Q41360"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2867932$A9EE34D3-EED5-47AE-BB04-EF4E3EBCFCAC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"2e07b63a7544a6d7c83390f82ddae368b77e124c","datavalue":{"value":{"entity-type":"item","numeric-id":19570,"id":"Q19570"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2867932$6CFD15D2-9F4F-4129-98C6-AE0CD4E76270","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"f1efe251f10f20310d9fc2391ac64c314c66eb36","datavalue":{"value":{"entity-type":"item","numeric-id":19751,"id":"Q19751"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2867932$604F6DE6-9028-4D61-8F8E-2A6CA880E2E8","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":"Q2867932$C6300E38-3D24-461F-9194-EB0BD763EE0D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"dfc04cb9d60b5d55b254e88c83f4544e393bedf7","datavalue":{"value":{"entity-type":"item","numeric-id":14005,"id":"Q14005"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2867932$A9361777-E4B5-4951-8CC1-D1CED7EEC8F6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"9aeef25d5839625565921d83cf1c652bf6f2fbf6","datavalue":{"value":{"entity-type":"item","numeric-id":17052,"id":"Q17052"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2867932$0D8129C9-318E-4CFA-BD6C-A0888403D372","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":"Q2867932$1CD0F8B8-9FE9-4E96-96B9-342EDE7288B8","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"57081ed5a699d6012d66c80f44dcfebf0d8bbd83","datavalue":{"value":"https://doi.org/10.1016/j.entcs.2006.09.018","type":"string"},"datatype":"url"},"type":"statement","id":"Q2867932$8E5FABD9-5C91-4324-93EF-4283F84D406F","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"b59dd02e1bc5df4875c081ed6172751d776107e9","datavalue":{"value":"W2145365771","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2867932$E82DD896-1D06-4FCC-AA06-E0B278A8199F","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"0aad2711eb9c64a58dada485191047b8af29959d","datavalue":{"value":{"entity-type":"item","numeric-id":4040283,"id":"Q4040283"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2867932$ABFA0372-C5D4-4FB5-AE9D-C37A5ACF44DA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f8ab3e683fcf1f4589adbbb54eed5465c20ce3fa","datavalue":{"value":{"entity-type":"item","numeric-id":2867932,"id":"Q2867932"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2867932$EF852C37-5EC3-453B-9229-1A1328360D9B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a71712455a619c09bf3f52fa45ff271444532140","datavalue":{"value":{"entity-type":"item","numeric-id":5756741,"id":"Q5756741"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2867932$FD725844-3D15-4D41-8331-D0309B308E24","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"98052a8fe89669b2fe4131e688755f41384ea6a6","datavalue":{"value":{"entity-type":"item","numeric-id":5178875,"id":"Q5178875"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2867932$6F71E1AD-D54A-40E3-ABE6-224886E8EFBE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ffe62377108373cd046811a24014b149bc79d51e","datavalue":{"value":{"entity-type":"item","numeric-id":3543644,"id":"Q3543644"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2867932$A51F22C3-B7E6-47F1-87B2-58926BA648FD","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"dd2c62957673ebd1309197e2b5108ec0b39be944","datavalue":{"value":"10.1016/J.ENTCS.2006.09.018","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2867932$215533BF-EBB5-4699-9326-310EAA9E9B9B","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"dfd02dce4dfd94819e6b27f03cf88bd485d0337b","datavalue":{"value":{"text":"ACL2s: ``the ACL2 sedan''","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2867932$4CB3A84B-089D-4E96-85A7-F951CF7B4D3F","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"56d606835397ced889225aa24646e03238343394","datavalue":{"value":{"entity-type":"item","numeric-id":3000661,"id":"Q3000661"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7595a6e2bbc0c6379f62941dfa6f95917c22d247","datavalue":{"value":{"amount":"+0.8985278606414795","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":"Q2867932$3A0BE022-9BE1-4D16-A59B-9DCB10AFE96C","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":"241b1822a8704e974b49aeac05cfb0ea68bba68a","datavalue":{"value":{"amount":"+0.8220915198326111","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":"Q2867932$AAA33B22-D30C-4946-BEF6-41AF6A99FB35","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"15d76b42d1c936c5ae7793777e9f9178a1e4946d","datavalue":{"value":{"entity-type":"item","numeric-id":5083764,"id":"Q5083764"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6ac4382e39842e57c1fd0d1f194de808b9305045","datavalue":{"value":{"amount":"+0.7857102751731873","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":"Q2867932$DBF2F6E1-747B-4C72-8115-6FB9B47B25D0","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":"e9bd6d99e1305278d98c2eb8cece889353bdda7a","datavalue":{"value":{"amount":"+0.7846865057945251","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":"Q2867932$B5F3AF91-3204-4AA3-B7F9-C8831FECD60F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3866260072cf2859e4d234424d2722aea9ea4298","datavalue":{"value":{"entity-type":"item","numeric-id":1595929,"id":"Q1595929"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"039501140e97ca32c756ce4f609d9c0b5d3f0b9a","datavalue":{"value":{"amount":"+0.729550302028656","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":"Q2867932$338DAD84-1C25-4128-9011-E04C95E515ED","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:2867932","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:2867932"}}}}}