{"entities":{"Q6659923":{"pageid":14271080,"ns":120,"title":"Item:Q6659923","lastrevid":100174016,"modified":"2026-06-05T21:33:17Z","type":"item","id":"Q6659923","labels":{"en":{"language":"en","value":"Verified implementation of an efficient term-rewriting algorithm for multiplier verification on ACL2"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7964381"}},"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":"Q6659923$481919A4-4A59-4035-8E36-238E9FA317EA","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"03ca36dc3924cfe460fb872c1099ffd0bd1ce539","datavalue":{"value":{"text":"Verified implementation of an efficient term-rewriting algorithm for multiplier verification on ACL2","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q6659923$EADE89C2-8940-4F69-B399-C53D41A6B547","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"e5f356969c7248d10d06a0399bd8346726603f73","datavalue":{"value":{"entity-type":"item","numeric-id":2225122,"id":"Q2225122"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6659923$283B8EA3-06D8-44E2-83CB-18E2B9E6EC52","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"f4d97a11f2ce21fc62fce1ecd5bb5e80dc2dcc64","datavalue":{"value":{"time":"+2025-01-09T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q6659923$C67B6EAB-FFE4-4CFA-B407-4A44E144ECFF","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6659923$67511D2B-B957-43BF-93DD-D72815E89EB1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"cd80e9ade304e6b9b43fd50d0c3436276c3c217e","datavalue":{"value":"68M07","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6659923$641E8647-C6B0-4AB4-A5FF-F0E1C6B8E118","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"c636094cc8b933189eabd7c009d327f829bc6ac4","datavalue":{"value":"68Q42","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6659923$485D338D-7FC0-4260-AF9C-587839974CD7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6659923$E5D8D0F5-1C11-4F24-AAC6-34920D1CDBFD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"58b3a5d0bc4bfd215423308dfe52b6887acdeedd","datavalue":{"value":"68V20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6659923$27A34D19-7790-4BF7-87D0-89A0F513E2D7","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"d6bafffbd0d036afc184b9a1f9ff9ec4d87cae1b","datavalue":{"value":"7964381","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6659923$07BD98EC-31A4-4E1E-AA7E-459D6658EDF7","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":"Q6659923$D056907E-7F2A-4832-A239-551808CEAE0D","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"8eea5cef58cdda3de950fbc9dd56b5e194eca118","datavalue":{"value":"10.4204/EPTCS.359.11","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6659923$18AA5DBA-DE0E-49C8-9E45-C7A559E26F83","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"30de85ed16d9a2162c13d706232b2d7388026c5c","datavalue":{"value":{"entity-type":"item","numeric-id":2225123,"id":"Q2225123"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"997de99c5861e0d80669369c94f3c04109cd1a81","datavalue":{"value":{"amount":"+0.7805131077766418","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":"Q6659923$D1A084FE-C998-4A8A-98E4-D0FB2DD92745","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c8162a59b8a13ef31c7b2c2cfc782b60b654f3a3","datavalue":{"value":{"entity-type":"item","numeric-id":4503919,"id":"Q4503919"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"29376c5ea468142f38a5e38ef3ce3f478ab5491e","datavalue":{"value":{"amount":"+0.7297312617301941","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":"Q6659923$2C74AFD7-D95A-4B9A-8157-68F91C845CC9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4682ba7101b685f9765cfbc6e73d25a52e47e023","datavalue":{"value":{"entity-type":"item","numeric-id":6193697,"id":"Q6193697"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b84397a8b6f5dcc357f25adc330af2654ba3bb83","datavalue":{"value":{"amount":"+0.7261410355567932","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":"Q6659923$4D547E88-478B-4115-A0DA-22971C20D75C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"41869de0d161e512039592ed17633e5085e242d7","datavalue":{"value":{"entity-type":"item","numeric-id":6165885,"id":"Q6165885"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3202d684efcd44cc9ec1987bdfc598aa0273dc13","datavalue":{"value":{"amount":"+0.7182910442352295","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":"Q6659923$065C3135-5DB8-4323-BBC8-32B61188E871","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"13e649264ee8c5f77323097969c0d9813410c2c8","datavalue":{"value":{"entity-type":"item","numeric-id":2754046,"id":"Q2754046"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e5cb9c38ddba3db55b006d271de5eb83260bf8cc","datavalue":{"value":{"amount":"+0.7114429473876953","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":"Q6659923$1C4186D5-B523-474A-A6F0-DF70A4855C90","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Verified implementation of an efficient term-rewriting algorithm for multiplier verification on ACL2","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Verified_implementation_of_an_efficient_term-rewriting_algorithm_for_multiplier_verification_on_ACL2"}}}}}