{"entities":{"Q1610218":{"pageid":1620958,"ns":120,"title":"Item:Q1610218","lastrevid":68037462,"modified":"2026-04-12T21:01:17Z","type":"item","id":"Q1610218","labels":{"en":{"language":"en","value":"Formal proofs about rewriting using ACL2"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 1783440"}},"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":"Q1610218$37589BD8-B3EC-49FB-9998-BCEC0905668B","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"290ec9510ad0e024b2cbc533db242e900928ea96","datavalue":{"value":{"text":"Formal proofs about rewriting using ACL2","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1610218$3D8CB727-B67B-4DC6-A605-F55778804EF6","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"8b9dadc2c6685265e30b582b7209f5a29227774d","datavalue":{"value":"1015.68169","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1610218$8B9D5750-121D-4369-ABF8-7CD9525FD8C1","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"aef80d17dc09142060c49c9c32fc69320a06bd8a","datavalue":{"value":"10.1023/A:1016003314081","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1610218$6DE82A33-6D95-46C9-80F7-361E0D02F015","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"7346dc34d1d50fea46ec345fbc7e3214530889ab","datavalue":{"value":{"entity-type":"item","numeric-id":276517,"id":"Q276517"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1610218$5938A2E3-B925-4949-8E26-EA058FDF2E7B","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"0004237905b7322cb3b10a20c84f2f03323c8c30","datavalue":{"value":{"time":"+2002-08-19T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1610218$4C6B7299-DB52-4CBD-8786-F77B4AD4CCC4","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1610218$D83E36F0-9F26-444D-8E7D-68B1E51A19C2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"c636094cc8b933189eabd7c009d327f829bc6ac4","datavalue":{"value":"68Q42","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1610218$B7B0FC91-D64D-4B71-A4A8-BB8B0E59D597","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"c0c99f5309138ed7841d3eb5e29422d3de0bdca2","datavalue":{"value":"1783440","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1610218$742759A2-FFAE-4ED4-8D5E-150CA99C7194","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"22498cf86e242a38d9fe355523225aa55193233b","datavalue":{"value":"theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q1610218$D449E3CB-A2EA-4054-A0A6-A3FD0FD122E6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"24dd5926fa2c4f0ee181b086899e10f05b3e9148","datavalue":{"value":"ACL2","type":"string"},"datatype":"string"},"type":"statement","id":"Q1610218$0894D472-4391-4893-9E3B-9AF98921D011","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"476e70cc5d552d5cdc76575cc73d40a8bfb4b86e","datavalue":{"value":"rewriting","type":"string"},"datatype":"string"},"type":"statement","id":"Q1610218$0A1EF0A2-01EA-4406-AD38-6522159B3D13","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"2eb4d1af95699ef062cce80ecbcf1e1484586450","datavalue":{"value":"formal verification","type":"string"},"datatype":"string"},"type":"statement","id":"Q1610218$F9D60A84-CCDE-42BC-8841-E99A7FBD6F83","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f7f82e5b3fddf0920d7af80635fcdd17881d7b23","datavalue":{"value":"rewrite systems","type":"string"},"datatype":"string"},"type":"statement","id":"Q1610218$BD74A52C-E8F3-4C4B-A75B-893BB32CDFD8","rank":"normal"}],"P16":[{"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":"Q1610218$642A31D5-1017-45E3-9CF5-296083E18673","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":"Q1610218$12559EA6-87D5-4E9A-BAB5-4DE3EC126DF7","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":"Q1610218$B7DE9FB2-8057-4FAB-9100-F02D241DD472","rank":"normal"},{"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":"Q1610218$2C120150-AFE9-4BA5-93DD-94265E7A35C0","rank":"normal"}],"P1463":[{"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":"Q1610218$0B60F52B-C6CC-4449-9D63-DF511E6C327F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"233bd03fc74bc4c01e6f828569e5eb13f94bb747","datavalue":{"value":{"entity-type":"item","numeric-id":22242,"id":"Q22242"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1610218$9AC68704-B755-4D98-A5A4-8E546DBB643C","rank":"normal"},{"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":"Q1610218$993C1AB8-DDE2-4783-97AC-C8D0C1A15889","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":"Q1610218$71FA47AA-BCEB-492C-B910-66C4C16785B1","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d9c7e2906cab0df39eaaaec6ded4334d15f17931","datavalue":{"value":{"entity-type":"item","numeric-id":4471942,"id":"Q4471942"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2dd3531e8c6c29d2caa14b593ef17a0da68761a0","datavalue":{"value":{"amount":"+0.9643931","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1610218$C7518116-9AD5-47C6-9CA6-5812A3FB50E0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"cd7a205481490a7875a29fdeade9e7b77717a55b","datavalue":{"value":{"entity-type":"item","numeric-id":928668,"id":"Q928668"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"12b8233f7ff398dc183f0b0401be609c230309e9","datavalue":{"value":{"amount":"+0.9060737","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1610218$5A1CB7C1-B9C7-4108-AD0A-157FA00F070C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f5bdac2a0e62336004c23566aca5dee3507efa6e","datavalue":{"value":{"entity-type":"item","numeric-id":3408130,"id":"Q3408130"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3623200fdc482a306f2c934b84ff1bc1a28abb0b","datavalue":{"value":{"amount":"+0.8734597","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1610218$3E5077F5-CD96-490A-8A77-3675D9759EF6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"75e29f2fd55f70b23450ed98479c53a683b1ea6d","datavalue":{"value":{"entity-type":"item","numeric-id":2233502,"id":"Q2233502"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a71b55c4f3c9680c4b81da8691921818c94b3396","datavalue":{"value":{"amount":"+0.87071955","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1610218$32954DB9-DC7F-4431-986F-B0798A160319","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"760a14bfabc4e10a8a1363a170fc2f2ca225ee11","datavalue":{"value":{"entity-type":"item","numeric-id":3079919,"id":"Q3079919"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f7e4b396cda024b5a7011cad41b2e810f2fb9520","datavalue":{"value":{"amount":"+0.8705904","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1610218$699A24E9-3ACE-4376-AC18-EB363D1657BF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c6e02866bedcdddc38a6d5d0dc3312cefd57e45a","datavalue":{"value":{"entity-type":"item","numeric-id":2870142,"id":"Q2870142"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"afc37cb0841f1b018cc4d84841c00b46b696cfe6","datavalue":{"value":{"amount":"+0.86825216","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1610218$0D3BC092-C950-4B7A-AFAB-5E161D1B29D1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"fe141363dd9c7092b04d31f82a14c5ec11d3b540","datavalue":{"value":{"entity-type":"item","numeric-id":3527295,"id":"Q3527295"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7a52daca1fbb38929f4b08b1a0b47227e4dbecfe","datavalue":{"value":{"amount":"+0.86625147","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1610218$9A441F4A-AAD1-4775-B6DA-E18F511980F8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"983cd21deef8e8804b56013c2e7cdcc132ea1307","datavalue":{"value":{"entity-type":"item","numeric-id":2722043,"id":"Q2722043"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"180236da6dbf21d48db52fbe20edae95b10477df","datavalue":{"value":{"amount":"+0.86458564","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1610218$E3EFB4DF-E33C-49F2-8C90-53F7440ABD40","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"80c6a4f837fe677b1512f0a548a42f3f878d78b2","datavalue":{"value":{"entity-type":"item","numeric-id":3090877,"id":"Q3090877"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"253ac9bc74a912b5568c6af2442de2c6a04f2b7c","datavalue":{"value":{"amount":"+0.8615544","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1610218$FD48386A-AF4B-4B32-A3AB-863E9CAA5DE8","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Formal proofs about rewriting using ACL2","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Formal_proofs_about_rewriting_using_ACL2"}}}}}