{"entities":{"Q2870142":{"pageid":2880862,"ns":120,"title":"Item:Q2870142","lastrevid":83842358,"modified":"2026-05-07T12:42:36Z","type":"item","id":"Q2870142","labels":{"en":{"language":"en","value":"Proof-pattern recognition and lemma discovery in ACL2"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6247449"}},"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":"Q2870142$735EB734-2BA8-45CD-8F60-A4E867A2B60C","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"d2cf4cb5f660e0a46774a1ff4e9ea820437b6380","datavalue":{"value":{"text":"Proof-Pattern Recognition and Lemma Discovery in ACL2","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2870142$14CA8145-BE62-4DF5-AD28-C112A6ACE498","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"9ed74ad6b1b1e5f4a88cac2f7a3372b4276e5941","datavalue":{"value":"1407.68436","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2870142$3491F247-78CF-436F-B57E-588E610A8388","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"cb200baeb5371bbfd0a9d9d47f2198fcf6b6e6ae","datavalue":{"value":"10.1007/978-3-642-45221-5_27","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2870142$5B134815-923D-4BF7-91F5-3EF8D17EAC6B","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"bc9df023cae9b25ea4b60776547a8efc95e2e421","datavalue":{"value":{"entity-type":"item","numeric-id":280197,"id":"Q280197"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2870142$DC7EC8E6-5BF2-4EFF-9B3E-551AD344543F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"170e56a44d87084edf1707672598135a08e36b5f","datavalue":{"value":{"entity-type":"item","numeric-id":280195,"id":"Q280195"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2870142$A953E70D-945B-4F31-BAC0-B86A30B3734A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"0ff9a748cd6fc1ff0926984ae3ee01554f12fa14","datavalue":{"value":{"entity-type":"item","numeric-id":287274,"id":"Q287274"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2870142$6459D52D-7984-48D1-A14E-B844ED441A29","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"39eefdf43007a5db029de99b1444c96ff88fcb4b","datavalue":{"value":{"entity-type":"item","numeric-id":667525,"id":"Q667525"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2870142$D14AEA9D-4D4D-4642-9B2E-26D507278B7D","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"23864e2be568bb8a6a4b0526f5a5216348320070","datavalue":{"value":{"entity-type":"item","numeric-id":2870110,"id":"Q2870110"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2870142$9B724EAD-0DF8-4665-B18A-FE66276654E3","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"7cbcb8793fff212e9a1970116a64b7b67cfe92e5","datavalue":{"value":{"time":"+2014-01-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":"Q2870142$15A09200-8402-4DB1-8981-6A38F43455DE","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"bac28aadd51cdf3938ea66de69ff809d457821d2","datavalue":{"value":"https://arxiv.org/abs/1308.1780","type":"string"},"datatype":"url"},"type":"statement","id":"Q2870142$F632273D-10D6-4AA8-A268-F25BB76BBBAF","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2870142$99F61D17-FEAF-45FD-8955-C99AE059348F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"cfe779e91fe9c53ee133568259955801965765ae","datavalue":{"value":"68T05","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2870142$5CA36070-779E-468E-B3BE-CBB4372F1438","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"8a784276b4e09d379c8147965411b455c3d79751","datavalue":{"value":"68T10","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2870142$BEF4FF2C-69DC-412A-B100-0B1F6643ED62","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"07b0d09aeda385df5be101427b37c8a0ac7ce729","datavalue":{"value":"6247449","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2870142$F87D4396-78D5-4DFD-8AAB-2DC7424626EC","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"22498cf86e242a38d9fe355523225aa55193233b","datavalue":{"value":"theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q2870142$3A211E52-C486-4BD0-8BD4-6401B485270D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"15475605022e2eedc5a0d9f9a816fb3f3998890e","datavalue":{"value":"statistical machine learning","type":"string"},"datatype":"string"},"type":"statement","id":"Q2870142$9B17CE06-BBC3-4187-A620-7CB06D171029","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"b508eb9c171301d8939bcc797b0cd89d2ccbd533","datavalue":{"value":"pattern recognition","type":"string"},"datatype":"string"},"type":"statement","id":"Q2870142$591CEE0C-4917-43CB-819C-3F7D34B76AC4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1cab0fc5514ba914f481903d3e6b1d1c5f5d536c","datavalue":{"value":"lemma discovery","type":"string"},"datatype":"string"},"type":"statement","id":"Q2870142$88E52835-B3D0-4BB6-9C7E-C571662AF70A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"95f12682f64f5866e4b655585f66f88c75047550","datavalue":{"value":"analogy","type":"string"},"datatype":"string"},"type":"statement","id":"Q2870142$CD4CEC6A-28E3-4BC5-A802-A08C618B8622","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":"Q2870142$A041FD61-B27D-4219-883E-B7D098BA1571","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"0ecee973cce27aca9d6609100a6fb4d87c282d91","datavalue":{"value":{"entity-type":"item","numeric-id":19195,"id":"Q19195"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2870142$29CC7DE8-D11C-4E53-8B8A-D97A89660E6C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"62af2c5e450adf37bd9acb47c5a55b60b68447ea","datavalue":{"value":{"entity-type":"item","numeric-id":22241,"id":"Q22241"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2870142$15215824-B727-42CE-A172-920B3A760B94","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"4bf6b098c4c01159a1cdee4d92fe2d1a9384e1ff","datavalue":{"value":{"entity-type":"item","numeric-id":22353,"id":"Q22353"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2870142$0E07C57C-50C1-4B90-BD39-DAB9992BE8AA","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":"Q2870142$3879675F-2704-4FEC-9C55-5FA9BC958C5F","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"131e01633916cb226434c4108f91b9402a2cc3fb","datavalue":{"value":"W1549265610","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2870142$D9E97DD8-0B65-4F00-8ED8-0320002E3182","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1dfa61574fc575acc4cb7d0ca05a72ef1b08a526","datavalue":{"value":{"entity-type":"item","numeric-id":2287904,"id":"Q2287904"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"af0b4b430ce27a864a956c154f76959c9dd0afcc","datavalue":{"value":{"amount":"+0.7702735662460327","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":"Q2870142$3F595FCE-DEA0-43BA-A190-EFF61A09980B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"eb636f355d8796679a448ab2f0465b71bf2a95f4","datavalue":{"value":{"entity-type":"item","numeric-id":3459922,"id":"Q3459922"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7ab0e79f7bc2d94cdbaffb42c4803f0198085874","datavalue":{"value":{"amount":"+0.7680683135986328","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":"Q2870142$228D36F0-C970-4322-81F0-BEA9A1CF125B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"14b8b36929715000acf1cd883b9b1d7bc9f1ba30","datavalue":{"value":{"entity-type":"item","numeric-id":475385,"id":"Q475385"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"bc304a9342690a45b400b065f42a1b540f8d3243","datavalue":{"value":{"amount":"+0.7421377301216125","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":"Q2870142$63DBE001-33F2-46C5-8CF4-FC8496223F5C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0ee8b4c79deb3aa57ce2641b4039a91462d9cc63","datavalue":{"value":{"entity-type":"item","numeric-id":4465166,"id":"Q4465166"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"fc0a87b3103af8b21a69ce80ecdfaec236f61101","datavalue":{"value":{"amount":"+0.7396965622901917","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":"Q2870142$EEFAFF1E-91C1-4009-8E51-69F80608F443","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"733045d4bdb6ac84e39d437da15db86acd1c641d","datavalue":{"value":{"entity-type":"item","numeric-id":6108816,"id":"Q6108816"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7d9ac6377e44f2f513fd3372f657b72841092ccd","datavalue":{"value":{"amount":"+0.73764568567276","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":"Q2870142$0D4243CC-A6A7-4506-B194-DDC2E62B8E14","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Proof-pattern recognition and lemma discovery in ACL2","badges":[]}}}}}