{"entities":{"Q2642461":{"pageid":2653204,"ns":120,"title":"Item:Q2642461","lastrevid":50145899,"modified":"2026-01-13T06:44:14Z","type":"item","id":"Q2642461","labels":{"en":{"language":"en","value":"Theory extension in ACL2(r)"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5179881"}},"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":"Q2642461$D494AA36-3B02-4670-9D8C-2C227B348042","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"b60cbb25a7e16fa935a6c7f5b8b2b42e66e46536","datavalue":{"value":{"text":"Theory extension in ACL2(r)","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2642461$C1403119-8A83-4D78-8162-17AC2933D89B","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"7645d1ecd704f59cb6f59acffc5c6c8a1ad78301","datavalue":{"value":"1118.68651","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2642461$9E3BC713-D461-4151-9E1B-65846B30A93B","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"b84cc8b5923f45dc86ae69f67f68bf56d7ecfce9","datavalue":{"value":{"entity-type":"item","numeric-id":174771,"id":"Q174771"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2642461$FE0CDA99-030C-4FA9-8F01-C9F8676A2044","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"83e4c4eb0c7bbbd668895e6c0cbc0b4f249cfbea","datavalue":{"value":{"time":"+2007-08-17T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2642461$A79D0824-CB64-46BC-B3B4-4ABEF6AD6892","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2642461$36FC10D0-DDBF-4951-BC85-1D87AAB0D1C4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2642461$8A72D119-6633-4BC9-A957-5191A27A5803","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"a22eb1f642cbb79777784e33676c61b720925aab","datavalue":{"value":"03H15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2642461$942CB1D0-B592-4BE8-B5DD-ADC028140F6C","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"2eca64a120c8beb6ba6598f2ce0c1adb39ede426","datavalue":{"value":"5179881","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2642461$6FA22F43-7A61-4552-A2F9-84A6E1FBB4FD","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"8bf549142b710f01581b24fd28cbb67614316cd4","datavalue":{"value":"theorem prover","type":"string"},"datatype":"string"},"type":"statement","id":"Q2642461$165A2E18-7B8C-4EBD-947A-6A5771560636","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"53de145c1476af14e05c31ec8165f08e3c85436f","datavalue":{"value":{"entity-type":"item","numeric-id":230813,"id":"Q230813"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2642461$ADE3C71C-6D0B-4306-BCAD-EFEAA5D25262","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"d3064c548fb238d71dbd15832dc9b2117bf93634","datavalue":{"value":{"entity-type":"item","numeric-id":1135305,"id":"Q1135305"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2642461$D3574259-B109-4BA8-B4FA-31C1A9420612","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":"Q2642461$F1D5A7AC-1282-4B48-836B-9832318974F4","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":"Q2642461$2A22F90A-FAA5-40C3-BC58-18BB0B1704E7","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":"Q2642461$013D375A-2AC5-4EB2-B52E-76D11D6E7C6A","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"a83864308c7e13513fa63c5f18b4e0650c20422e","datavalue":{"value":"https://doi.org/10.1007/s10817-006-9043-0","type":"string"},"datatype":"url"},"type":"statement","id":"Q2642461$96215977-D85A-4996-BC03-52B606F1ECD6","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"3cd1b35fdba1a1e07375a33d19a108228d567a55","datavalue":{"value":"W2080350563","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2642461$9A183A90-D261-403C-9251-7C1C624B5319","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"283b457c1aa928df8cba388628638010a8a9e043","datavalue":{"value":{"entity-type":"item","numeric-id":4016540,"id":"Q4016540"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2642461$5FA60D78-CE55-470D-81EA-E65019304FC7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8124e2aa86067094dab23bb14b8dadf2e19d522b","datavalue":{"value":{"entity-type":"item","numeric-id":3894958,"id":"Q3894958"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2642461$ABCCBA61-541D-44DB-91DB-2E5A94C719E0","rank":"normal"},{"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":"Q2642461$2E9B5244-4883-4F59-B8BB-830D63CE2544","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d3c43ad45aa5b3a97181ec14ca3061a69c8be3de","datavalue":{"value":{"entity-type":"item","numeric-id":1905745,"id":"Q1905745"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2642461$DFFB55B6-455F-4293-AC9A-656AC450FC99","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"eaab286ce9532044a0bbcada18389d4ffcc9518d","datavalue":{"value":{"entity-type":"item","numeric-id":5956117,"id":"Q5956117"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2642461$76BB069E-AE75-4E96-9F35-AC70963CAC32","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1eff1a1596e89669a389607aa485f25f25de9fc8","datavalue":{"value":{"entity-type":"item","numeric-id":4821145,"id":"Q4821145"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2642461$74503D03-0F7C-444D-B9F3-039ED5ED9857","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ca6926d9a2864657c63c8ba6d81f03198b036942","datavalue":{"value":{"entity-type":"item","numeric-id":1595929,"id":"Q1595929"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2642461$769D0876-D300-46F3-8F3D-D5245F4FC6AE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"bec2770e1b1bced5acaf1a085e30e72a51ee32bf","datavalue":{"value":{"entity-type":"item","numeric-id":4149449,"id":"Q4149449"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2642461$3ED1C6B1-6270-4FEB-854D-2F1263A2F2FD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"96f977d68eabaf6bf4143bba3925a079e66ebb8a","datavalue":{"value":{"entity-type":"item","numeric-id":4039861,"id":"Q4039861"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2642461$43C2B0B2-7698-42CA-BE37-81F171B4B096","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9c7464923d81853deaa10ebf504925145345ff75","datavalue":{"value":{"entity-type":"item","numeric-id":4870980,"id":"Q4870980"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2642461$D9C5FF74-BE77-4E88-8B11-EB4132153A0A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0ec407bff047c5b2a446c4eab8012ded481f5def","datavalue":{"value":{"entity-type":"item","numeric-id":4427909,"id":"Q4427909"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2642461$82EB642B-254B-479C-8ADE-2203C3E4661C","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"dd8e64a36e9ebdff247e4550650d40937d58162d","datavalue":{"value":"10.1007/S10817-006-9043-0","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2642461$CC52515A-8A88-4721-9CC0-B44E88724278","rank":"normal"}],"P1643":[{"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":"9a315d92a18d44ab33292ed474acfb22e807cb71","datavalue":{"value":{"amount":"+0.8805520534515381","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":"Q2642461$7C8A35D2-0089-4ADD-B06E-B1A5BA301287","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7ec9048f0c16019dacc5a2b0ff53606251c8e48b","datavalue":{"value":{"entity-type":"item","numeric-id":5897076,"id":"Q5897076"},"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":"Q2642461$3733D9E9-F158-4B74-A9F8-77DBD4DE1787","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"52785f2dd2003261c737010c9dd8c0d12eaa464a","datavalue":{"value":{"entity-type":"item","numeric-id":1334896,"id":"Q1334896"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"83c2f55945616b51d8bb63d8161ddbd0c2461d53","datavalue":{"value":{"amount":"+0.7507834434509277","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":"Q2642461$F169D5DD-4B79-4F8A-A2AF-B12F309A6E73","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e13f94efa5a180ee860e2173b41929c73d33793f","datavalue":{"value":{"entity-type":"item","numeric-id":4231030,"id":"Q4231030"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"496395a707063485d27a86cd7a55ee9c8cd276b0","datavalue":{"value":{"amount":"+0.7364892363548279","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":"Q2642461$E880CF7C-CD7F-4A83-9116-A5E2EDAFE0F2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"afb714d42d44aae2ccfbff437eb23fd0a25261c1","datavalue":{"value":{"entity-type":"item","numeric-id":4504968,"id":"Q4504968"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b648264cf7bffc39ac23123ba83915da1002c5cf","datavalue":{"value":{"amount":"+0.7351546287536621","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":"Q2642461$2BD9C4F9-F838-4A54-96D6-E9144E6D1CD4","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:2642461","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:2642461"}}}}}