{"entities":{"Q1034553":{"pageid":1036401,"ns":120,"title":"Item:Q1034553","lastrevid":69472650,"modified":"2026-04-13T07:14:17Z","type":"item","id":"Q1034553","labels":{"en":{"language":"en","value":"A verified common lisp implementation of Buchberger's algorithm in ACL2"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5626909"}},"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":"Q1034553$E50AD34C-72A1-4971-AF8B-8E5934DC7CCD","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"c550f49112ace1925138a5321e8a0a13fdda9ddc","datavalue":{"value":{"text":"A verified common lisp implementation of Buchberger's algorithm in ACL2","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1034553$535AD935-2B0C-4C43-948D-BB420F768111","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"0548710ad722b0ad19342d40f82d6f7cb585711d","datavalue":{"value":"1194.68155","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1034553$AC11681F-53CD-41A1-AEFD-E4489BF68EFB","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"4db8fe7d2d486c28b44bdcfa5c3f02f800a9bc12","datavalue":{"value":{"entity-type":"item","numeric-id":1034551,"id":"Q1034551"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1034553$433A7FAC-E1FD-4E3B-9A65-14B08A01B881","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"fb2a59fbaee67f08ed7d3961700fd727ee3b0218","datavalue":{"value":{"entity-type":"item","numeric-id":1034552,"id":"Q1034552"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1034553$FFCA4B1B-7921-4B09-9BDB-0E182B9BC4EC","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":"Q1034553$B170BED5-6782-4BD3-9115-A98F6369A209","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"ea72303f92787da89554ee5fa15621068821a762","datavalue":{"value":{"entity-type":"item","numeric-id":99061,"id":"Q99061"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1034553$0BBF96F1-0255-4174-9D54-BC1A734AE5DF","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"5c80b38051786df2940873db0a591fda80f5fbfc","datavalue":{"value":{"time":"+2009-11-06T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1034553$A2715585-FF04-4673-B7C3-7604C1514BF0","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"092d9a7dfbbaaa84ba458f8d83190fce94c9aa54","datavalue":{"value":"68Q65","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1034553$39E54DA0-4193-4A54-A610-A4D9E1731CFB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"173b0c3afec7c4f9f987722665cc7bdb6b8f5813","datavalue":{"value":"13P10","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1034553$E4F2E9BE-28EF-4FD5-BA2B-40D227A4F3FA","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"764a2c8a7866ff4b02409d431d018353e2f46ec4","datavalue":{"value":"5626909","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1034553$746CD058-C565-42D5-B8C7-D697DCA74BE1","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"2eb4d1af95699ef062cce80ecbcf1e1484586450","datavalue":{"value":"formal verification","type":"string"},"datatype":"string"},"type":"statement","id":"Q1034553$296998D4-192B-446A-A09E-5F547C98491C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"24dd5926fa2c4f0ee181b086899e10f05b3e9148","datavalue":{"value":"ACL2","type":"string"},"datatype":"string"},"type":"statement","id":"Q1034553$359B1922-8E66-4C4E-9069-3835C264ABC0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"25a0d0a64145a26d41eb5308b1cb512dc20d7b36","datavalue":{"value":"computer algebra","type":"string"},"datatype":"string"},"type":"statement","id":"Q1034553$5210A760-3B0E-44B5-A177-83D7F426E025","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"698542b58ea564916b2ef53688be87fbd4e7199e","datavalue":{"value":"Buchberger's algorithm","type":"string"},"datatype":"string"},"type":"statement","id":"Q1034553$5D0790A8-B639-48BE-B3C0-AE3DFB482A4D","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":"Q1034553$0C535CD9-500B-47C3-9447-2970C90C1393","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"261ae6dfeffd96c9ea238e124055221c78337064","datavalue":{"value":{"entity-type":"item","numeric-id":13705,"id":"Q13705"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1034553$DB254927-A60F-48E3-8ED7-981B444C31F3","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":"Q1034553$C8F7A316-E721-43D9-8B5B-2DB3253B5771","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"19c3232540dc15c9350e8393498317de25361cb2","datavalue":{"value":{"entity-type":"item","numeric-id":16873,"id":"Q16873"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1034553$79B1A72A-2FBE-4436-9E8F-1F2FF79DF4FB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"a8f057223c758d6b8295ecbdef4842faac2ccb72","datavalue":{"value":{"entity-type":"item","numeric-id":19253,"id":"Q19253"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1034553$D0E6FF1C-3FD1-42A4-8977-80342622EC6A","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":"Q1034553$EFC13231-A863-4599-B40B-55D8762B0B07","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"f4a384a03ab30cd6b24715d92db14403e9cbd7d3","datavalue":{"value":"https://doi.org/10.1016/j.jsc.2009.07.002","type":"string"},"datatype":"url"},"type":"statement","id":"Q1034553$B1F7FDCF-2D7E-4B14-8468-852E0739B501","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"746591125342768402af314b3a2868627c20a39b","datavalue":{"value":"W2004470082","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1034553$22F8B24F-B566-4E2C-9E20-E53779891B96","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"60cfb58293fe4996506d53591cb886420c558f5d","datavalue":{"value":"Q57834883","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1034553$9EA82092-4764-4998-9DE6-124739032271","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":"Q1034553$973F6884-0BEB-445A-A2FB-46DD0B344041","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5d87900de754ad2a3f7d55a3f915d6adeffa7325","datavalue":{"value":{"entity-type":"item","numeric-id":2544438,"id":"Q2544438"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1034553$6B9BD533-175A-475D-9C7D-86A319788920","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f2e18fa15bf263a19b23697794f7b1453caff81f","datavalue":{"value":{"entity-type":"item","numeric-id":3021905,"id":"Q3021905"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1034553$4E5FE882-EA0D-48E8-AB8D-065AE4540599","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"48933c0d362727730cc1905c68ff87e3a22216cf","datavalue":{"value":{"entity-type":"item","numeric-id":2457345,"id":"Q2457345"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1034553$5E029C39-0E64-4230-91F9-7FD56BB72BC7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1616035475940e78f5e7ffe6b447afdd22db3a38","datavalue":{"value":{"entity-type":"item","numeric-id":3416408,"id":"Q3416408"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1034553$E3414DC0-143C-4E03-8F05-F6D1929F30C0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c7e013849775846918727fac3e7e6455bd448813","datavalue":{"value":{"entity-type":"item","numeric-id":865646,"id":"Q865646"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1034553$3FF6BAE2-F2CE-4CC8-9920-5F3721CBFAA1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6638576146949e050869fbd017d1f5e9c8d5e17b","datavalue":{"value":{"entity-type":"item","numeric-id":4377762,"id":"Q4377762"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1034553$F20A484D-B547-4843-905E-B0AA2463AE40","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0b1174e25682c6db55f75a0aae038d55e05f0e39","datavalue":{"value":{"entity-type":"item","numeric-id":4944848,"id":"Q4944848"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1034553$E3E51F57-2DE3-4135-A673-BB7EE2AFD91A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d8ba154389a204d2fe13cce852c6d6422d7912c2","datavalue":{"value":{"entity-type":"item","numeric-id":4023676,"id":"Q4023676"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1034553$FEDF0371-9822-4443-8520-5483CFED40C7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"100bb1ccd2c2d9635aec4ef9416ea5fe826fe553","datavalue":{"value":{"entity-type":"item","numeric-id":5437032,"id":"Q5437032"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1034553$1A78D753-C01A-4D5D-B362-A1B4FC069E40","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c4582c5ecaa6154cdd34ec4458b7d628349fce71","datavalue":{"value":{"entity-type":"item","numeric-id":1012152,"id":"Q1012152"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1034553$2A588BF4-FD22-4EF6-900A-1620FE7785EE","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":"Q1034553$3858BC9D-EC3C-429C-98B0-629B1C193174","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":"Q1034553$0A199FEA-A536-4B74-81F0-EEE36746A927","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ec326779be5f4f8dc3a81efc985f00f310bbe46b","datavalue":{"value":{"entity-type":"item","numeric-id":597122,"id":"Q597122"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1034553$46507C34-F375-4D27-864F-52FE821B5F06","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"185924672466c333b2a4f60179da234e4df54e65","datavalue":{"value":{"entity-type":"item","numeric-id":1610218,"id":"Q1610218"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1034553$72128D28-0AD2-42FB-920F-BD20BC943E18","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"04aaaa6c54da135216e6a5062ac0663af21a8a80","datavalue":{"value":{"entity-type":"item","numeric-id":5898527,"id":"Q5898527"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1034553$D761DFFF-3CE4-471F-8D88-BB663B017344","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b7536e92384e11ec3ce8637ede805331f9e036d8","datavalue":{"value":{"entity-type":"item","numeric-id":3997095,"id":"Q3997095"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1034553$1D6C0382-3D85-4B2A-9CF3-6F49F616FB54","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"36b04f8e06bc6d45cea746bdfc009dd75dad2987","datavalue":{"value":{"entity-type":"item","numeric-id":1595926,"id":"Q1595926"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1034553$9FE4B1FD-2A3C-4BE3-B537-A12B69023E19","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"fd23730217a332e3d4b05407f19a99fdbeffda0f","datavalue":{"value":"10.1016/J.JSC.2009.07.002","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1034553$5A229EBD-0030-4B87-9ED0-39E9AD435A92","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8bc953dd1614a07144d617fb2b8a68487cd9ef5d","datavalue":{"value":{"entity-type":"item","numeric-id":5464700,"id":"Q5464700"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c05bbe7e8c08c2dcf5718a8b1a0cf942469813bd","datavalue":{"value":{"amount":"+0.9082810282707214","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":"Q1034553$F33B1D88-8062-4BF5-BF1C-519447CA88FA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"95abb6469afc8d880f03764fc22c99f814d78278","datavalue":{"value":{"entity-type":"item","numeric-id":1798967,"id":"Q1798967"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ac97888701106ac29eafe2f12481e5c40594d403","datavalue":{"value":{"amount":"+0.7719588875770569","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":"Q1034553$91AFE109-0F78-4C83-AD67-7E1B640EF887","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"64fa174be350d15f32719e74a3c9677639f35386","datavalue":{"value":{"entity-type":"item","numeric-id":5394418,"id":"Q5394418"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"959609977016ee85a33eebc508ee57e2362a5ebb","datavalue":{"value":{"amount":"+0.7561578750610352","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":"Q1034553$D3BB0E96-F7E7-4E7A-8FC3-A3FCCC7D1253","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c160088cf25b70d48dfb6c6d0df5e8c0b8a72f7f","datavalue":{"value":{"entity-type":"item","numeric-id":4249903,"id":"Q4249903"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d18e8427bbad8bfab581c4d82d1b1da072da7c18","datavalue":{"value":{"amount":"+0.7525572776794434","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":"Q1034553$21819E8E-8DF8-4913-A484-65E205131233","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"fa9ee5dacc74280ba2bf4401bdf617ae6b1186a7","datavalue":{"value":{"entity-type":"item","numeric-id":2028994,"id":"Q2028994"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"44aa6ea54c8b3c8b60fb2c80384ce4575fe70c64","datavalue":{"value":{"amount":"+0.7291470766067505","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":"Q1034553$0C6CB4C4-0468-4B70-B2FB-361341C62DC3","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"A verified common lisp implementation of Buchberger's algorithm in ACL2","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/A_verified_common_lisp_implementation_of_Buchberger%27s_algorithm_in_ACL2"}}}}}