{"entities":{"Q438550":{"pageid":440317,"ns":120,"title":"Item:Q438550","lastrevid":51520322,"modified":"2026-01-18T15:00:44Z","type":"item","id":"Q438550","labels":{"en":{"language":"en","value":"Proof pearl: a formal proof of Higman's lemma in ACL2"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6062053"}},"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":"Q438550$3740EC01-8488-4329-9B44-6D6AFF480F2E","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"8d6e506d33a7a75015376933ea7920f0681d2dab","datavalue":{"value":{"text":"Proof pearl: a formal proof of Higman's lemma in ACL2","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q438550$911FD714-9372-42BF-86A3-2909A2A7A58A","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"9dffed459fe2f9415e88bf7a3bdabc54913bcd19","datavalue":{"value":"1243.68269","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q438550$1E0BDA91-3528-4C30-8554-F3B48974250B","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"76b38168777167ff49199bd7f47bfebb8e51e498","datavalue":{"value":{"entity-type":"item","numeric-id":438547,"id":"Q438547"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438550$ED6606EA-3FC4-45B0-8323-38AEACB171FC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"3c5989ab1028cea7e9ee7fb42127fc02a808a197","datavalue":{"value":{"entity-type":"item","numeric-id":438548,"id":"Q438548"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438550$EF956090-9729-49BA-9F52-5D0FA833822E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"dc442b6d258731aa6f56db3b1030762f889ec8e6","datavalue":{"value":{"entity-type":"item","numeric-id":417948,"id":"Q417948"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438550$1A00C730-5D26-43CD-9620-0A19A1992B1B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"7ab7d4636d237c78cfef4f47fdbac4805f8a7b82","datavalue":{"value":{"entity-type":"item","numeric-id":438549,"id":"Q438549"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438550$DEC8E252-A597-4E03-86CF-AF81C62CBF9D","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":"Q438550$547B4E79-CD06-4206-A3F0-370DE1EBC7A4","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"6c7ad691786690cf86127845d28cf47311748286","datavalue":{"value":{"time":"+2012-07-31T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q438550$9B4F1E05-AE2B-4F35-B359-670D453B03DC","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q438550$3AF3C294-A6A0-4265-B1E1-4A56C6E42ED2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q438550$30DB681D-2676-40DD-958E-92533C611034","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"da00c812255bd7f02dddc14c65a56e042cf0446e","datavalue":{"value":"03E05","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q438550$4B96603E-4EE5-4724-8DE5-959E1E6BD24B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"6247f04fad65d359a20e559b3e9499d6219d492e","datavalue":{"value":"05A05","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q438550$00BF634C-6207-4D07-A7BA-FC1D4545A8BF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"749b7137f279a66a306e75e15f613231b281c1c5","datavalue":{"value":"05C85","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q438550$A4DFBB07-AC83-4786-BFEC-615F72086481","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"86d6956f10f06a6edfda5d09b89e2fa018c5ae5e","datavalue":{"value":"6062053","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q438550$FE7DF4B6-17C1-41F2-A158-0A03BF8A15FD","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d39209d488652367428ee47b9a50e6491f07de09","datavalue":{"value":"Higman's lemma","type":"string"},"datatype":"string"},"type":"statement","id":"Q438550$F6B2C2A7-FDEA-4BB2-8702-84D41FA77A14","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"55caf05c57404ab910cf1d6d785d791abcc73ea3","datavalue":{"value":"formal proofs","type":"string"},"datatype":"string"},"type":"statement","id":"Q438550$D173DDBB-348A-4409-BE8E-1F0DB9A9F736","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"24dd5926fa2c4f0ee181b086899e10f05b3e9148","datavalue":{"value":"ACL2","type":"string"},"datatype":"string"},"type":"statement","id":"Q438550$BEBDA218-5E5C-4F7D-A4F7-9DE25862AE9B","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":"Q438550$DE3130F8-0A29-45FB-8CE4-F46346397B30","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":"Q438550$14FE778F-B92E-40C1-8C64-90E6BFA5A892","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"edf75882e3541445a013fdd01de3c2b33d7a19b2","datavalue":{"value":"https://doi.org/10.1007/s10817-010-9178-x","type":"string"},"datatype":"url"},"type":"statement","id":"Q438550$01266659-E1BE-41B4-9B43-A71B6522CC41","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"24d133bef8b4a77c4a5c62dbc36c9e9e9c703062","datavalue":{"value":"W1964096523","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q438550$19429D1B-9E72-4CF8-89B6-47D429547D9D","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"966399881400f3c28ab50ee13f3e7c96d9862129","datavalue":{"value":"Q124838861","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q438550$B8B476D1-4F21-4C40-AF37-CF8B42C450E1","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"819a2535befb2a67f49ee5e43432525215be36de","datavalue":{"value":{"entity-type":"item","numeric-id":4702972,"id":"Q4702972"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438550$4364AAD9-99D0-41B5-BF42-00FE132FB305","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"eeddfec2d6761bcca5b706cfa4f21836083ab429","datavalue":{"value":{"entity-type":"item","numeric-id":5712322,"id":"Q5712322"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438550$993FF60E-3287-46D5-BD7F-ADBB9FA0E528","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b27d44a0e50fda314668a36654efb04ab5135cb3","datavalue":{"value":{"entity-type":"item","numeric-id":3868730,"id":"Q3868730"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438550$6E017C37-93E2-449A-AF64-2A8087FA938C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2b977cc0abbb9233e203718261068766885e4fb3","datavalue":{"value":{"entity-type":"item","numeric-id":4246946,"id":"Q4246946"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438550$A56DB7AB-4F51-4DF7-8223-970268B63A46","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"58709679cfff7718457ae5dbfaa34a4e9b17219c","datavalue":{"value":{"entity-type":"item","numeric-id":5812263,"id":"Q5812263"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438550$3BC2599E-64EF-4EA0-A2BF-732AF18F99C4","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":"Q438550$9A9C0BDC-9015-4014-9BF7-77D24C9D2010","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c8a8f79ed5846190c4330090f3455868862b25dc","datavalue":{"value":{"entity-type":"item","numeric-id":3408130,"id":"Q3408130"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438550$1F4EC5F2-35BD-4304-904C-C6BE7034100C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"984b1d80654e94fcc7a819e892ad713c68332466","datavalue":{"value":{"entity-type":"item","numeric-id":5477667,"id":"Q5477667"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438550$50CF7B15-1E10-4D7E-A30C-6F59D910DBE9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0ed0853d5d25943754f0b88d3bc5a4e688b584cb","datavalue":{"value":{"entity-type":"item","numeric-id":5734436,"id":"Q5734436"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438550$8605B9CA-6DC8-4828-8EE9-A66DDB260374","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"20d8ad24cb4bd25b66b08a8a88a01461662f8272","datavalue":{"value":{"entity-type":"item","numeric-id":1803588,"id":"Q1803588"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438550$EE5ECDED-79A0-41C4-AFE7-902C47E4DF15","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"fa232931057b30d811aacaec588c82555ffa80ef","datavalue":{"value":{"entity-type":"item","numeric-id":4664924,"id":"Q4664924"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438550$424BC1A2-6FD3-4DD1-B18A-981D54CAC66B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f94056ab270f784a776b098fd21c488af8c94e39","datavalue":{"value":{"entity-type":"item","numeric-id":4736401,"id":"Q4736401"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438550$1E3BD152-9216-427E-B063-1A0016E97DCA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"836c0e3dce5c3c3f1796b886735793572a441d10","datavalue":{"value":{"entity-type":"item","numeric-id":3809796,"id":"Q3809796"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438550$259677EA-4CB1-4313-B791-23B59CBF4129","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"44767b6e6005554db2ca5db360b3405c87518bfd","datavalue":{"value":"10.1007/S10817-010-9178-X","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q438550$EE773077-EAF3-48E7-ADA1-5A4A785C7E57","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"74fcf341e56eb6ee74155d07e9b0e438d2a5b766","datavalue":{"value":{"entity-type":"item","numeric-id":5477667,"id":"Q5477667"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2a24fe7d96881f17ff1427abdb39e61dd611e592","datavalue":{"value":{"amount":"+0.9573203325271606","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":"Q438550$2C0AB267-A78D-4991-851B-D181779E914C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9fffdb80b08a4eeb186813621408a53ad1eea90a","datavalue":{"value":{"entity-type":"item","numeric-id":3305561,"id":"Q3305561"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a6713dd6c35feafec512e042734249261fc98c42","datavalue":{"value":{"amount":"+0.8531651496887207","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":"Q438550$F62B427E-7389-4D66-9E0C-19ADBD39F78E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1ce93b36fbb93578ad5ecba2c0a0680a8f43e366","datavalue":{"value":{"entity-type":"item","numeric-id":5712322,"id":"Q5712322"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"625b823f84185f439f0428095f24e2d6b8448aee","datavalue":{"value":{"amount":"+0.8400918841362","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":"Q438550$F9AF718A-EB89-4262-B458-72FEE2C5D297","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5646a8e54fc64977dc8dbf952c8c59395c9dc7fd","datavalue":{"value":{"entity-type":"item","numeric-id":4246946,"id":"Q4246946"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"334375a6733997c68068c08c7237c0aa249a4ed4","datavalue":{"value":{"amount":"+0.8332772254943848","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":"Q438550$DEFC9D4A-C006-4383-B81D-E461B2E8BFAE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e8be61ae365ac66846a3a9b92c68c400eb0ddb96","datavalue":{"value":{"entity-type":"item","numeric-id":5195254,"id":"Q5195254"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"334375a6733997c68068c08c7237c0aa249a4ed4","datavalue":{"value":{"amount":"+0.8332772254943848","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":"Q438550$6F5CC1F0-2EF7-44BE-9150-398E06921901","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:438550","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:438550"}}}}}