{"entities":{"Q3523181":{"pageid":5553085,"ns":120,"title":"Item:Q3523181","lastrevid":80636777,"modified":"2026-05-06T16:39:27Z","type":"item","id":"Q3523181","labels":{"en":{"language":"en","value":"Automatically Translating Type and Function Definitions from HOL to ACL2"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5318949"}},"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":"Q3523181$1336474A-C95D-4A99-851D-6A4CBF2B2864","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"017bb402d5ea473db75a440884c23112f7bc2392","datavalue":{"value":{"text":"Automatically Translating Type and Function Definitions from HOL to ACL2","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q3523181$4A2E74D9-4936-4721-A198-F23F702CA5D7","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"fe8c7acdc00205f22379701e9d17e3e1cc691bfe","datavalue":{"value":"1144.68366","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3523181$BF1818BA-054E-4BFD-AD98-43C41FF28667","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"ed39f1ff553562c6a6ebf7ef12d158b331139d66","datavalue":{"value":"10.1007/978-3-540-74591-4_20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3523181$EE9B9D33-8B32-404D-A728-162F2AE7A394","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"647c4a4d230c1041b2fbe0a4e7cec92e22c0b07e","datavalue":{"value":{"entity-type":"item","numeric-id":3523180,"id":"Q3523180"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3523181$57F6FB4C-7515-4D99-9183-6A611B273925","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":"Q3523181$F4AA2B19-D330-45A4-BE1B-B91FB60D5C06","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"20b7f535510e218ce28c7540c7cdc4660c15d850","datavalue":{"value":{"time":"+2008-09-02T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q3523181$19337E25-945B-4ACB-810C-4401B8F56DE4","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3523181$87585602-B1B3-4422-8C22-F3DCAF13B2EF","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"0ed4163f2acb31fabb87b1ec16cbb17072c109e4","datavalue":{"value":"5318949","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3523181$03EC9246-AC06-42E0-A30B-28ED846679E3","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":"Q3523181$3626AAB0-75DC-45F8-A518-3420B1E81C38","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"7f231912461a4cf859d87b4356c5e2a2037e1e84","datavalue":{"value":{"entity-type":"item","numeric-id":17631,"id":"Q17631"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3523181$488992F5-A858-42E0-AF0D-B009D8119CBF","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":"Q3523181$C2AFE3AA-91A6-46C2-9EF9-B94678079829","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"e6170b4af10414318cf423f9e5242d1faa8a1b5f","datavalue":{"value":"https://doi.org/10.1007/978-3-540-74591-4_20","type":"string"},"datatype":"url"},"type":"statement","id":"Q3523181$5084799E-6820-4E8E-9716-F511F6E5C321","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"df6f5416ae68687d7e8f46c055ebf978832a819e","datavalue":{"value":"W1595838964","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3523181$45897929-9CFA-4F2F-81E4-58E1F278A557","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5a89dd6970994c099e3030bbed6db81931530f4a","datavalue":{"value":{"entity-type":"item","numeric-id":5747659,"id":"Q5747659"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"16e94fa9e02f7a38d25890c7a0d36e8b316e58de","datavalue":{"value":{"amount":"+0.7925130724906921","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":"Q3523181$4BA7451F-137F-4B2E-9E22-F6BF7DA14DC6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8b7f4e39126d140b1fb7374f494c75cfd56020b6","datavalue":{"value":{"entity-type":"item","numeric-id":4790669,"id":"Q4790669"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"eee27ef133de0c85f158f47f04c33a5d2982fe38","datavalue":{"value":{"amount":"+0.7805705666542053","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":"Q3523181$3F0147A3-E3A8-46AA-9BFF-5DB173D124D5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d11280eec7f580346c0151d22527bb8d91725392","datavalue":{"value":{"entity-type":"item","numeric-id":2754039,"id":"Q2754039"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5cb898c64144e76b34116b9398809d2108892852","datavalue":{"value":{"amount":"+0.7664346098899841","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":"Q3523181$6F8230D3-D5CC-4CF0-9862-699969E9CA4E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f111eac5ad767c0299626bb8fc33167280082866","datavalue":{"value":{"entity-type":"item","numeric-id":2875232,"id":"Q2875232"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0425c26b294884eda8a578d49922d3f57d704d0d","datavalue":{"value":{"amount":"+0.7640586495399475","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":"Q3523181$585299CA-0526-4DE0-9184-ACC0832966CD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8b192e62cb80426c9f80cefc79bf866e47579f47","datavalue":{"value":{"entity-type":"item","numeric-id":5458345,"id":"Q5458345"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"411f97f9890898b3b91939027090fa9d55174b25","datavalue":{"value":{"amount":"+0.7588686943054199","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":"Q3523181$CB85A27E-A84A-465A-B314-BA5334167FD2","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Automatically Translating Type and Function Definitions from HOL to ACL2","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Automatically_Translating_Type_and_Function_Definitions_from_HOL_to_ACL2"}}}}}