{"entities":{"Q3100211":{"pageid":3110926,"ns":120,"title":"Item:Q3100211","lastrevid":58112979,"modified":"2026-04-03T20:49:06Z","type":"item","id":"Q3100211","labels":{"en":{"language":"en","value":"Tactics for Reasoning Modulo AC in Coq"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5977511"}},"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":"Q3100211$08F0B615-74F8-4C85-BFFC-56D9DC89E1FE","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"3a64f98017dee7cf3c3facea7720c0f24376a577","datavalue":{"value":{"text":"Tactics for Reasoning Modulo AC in Coq","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q3100211$5EC4B177-0AF9-4E6F-A514-7E90E16BB887","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"9584fa5af51b4daea42a2a140e5491aed6bd11e1","datavalue":{"value":"1350.68227","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3100211$E329EA09-4C54-47A2-9779-4AE76C525F98","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"c99caa474a54f02361db34e5edbdc7525b4a2b15","datavalue":{"value":"10.1007/978-3-642-25379-9_14","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3100211$D43B756D-D4FD-4907-A6D9-3170774C467B","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"12328682479f4a45e2f0e2c1b6bc2d9e6d8cbf3a","datavalue":{"value":{"entity-type":"item","numeric-id":2351421,"id":"Q2351421"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3100211$71086311-2DC3-41A7-909C-A425B823B3C6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"b609b0474903c90ee98ec931eee072d672864771","datavalue":{"value":{"entity-type":"item","numeric-id":299193,"id":"Q299193"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3100211$DE69A207-BDCB-4BDC-88DB-CF5135712226","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"19e7468504fbcb9c3a09d3a38cdd67d03e02eec6","datavalue":{"value":{"entity-type":"item","numeric-id":2938035,"id":"Q2938035"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3100211$61B1FFB9-EF68-4190-9046-B0CA0B63DE51","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"6d06d6de084d6566994eb3940381939ab0e2877d","datavalue":{"value":{"time":"+2011-11-22T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q3100211$53DA70F3-C713-44BD-90C6-EA51A01CEC89","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"ecdac2abe88f6fc525e1e6e08a5908044e02272d","datavalue":{"value":"https://arxiv.org/abs/1106.4448","type":"string"},"datatype":"url"},"type":"statement","id":"Q3100211$5EAEE9FD-BB11-476A-A3B0-C723A5E58F81","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3100211$E95806EC-E9DE-488D-B954-1BEDB44CC88E","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"041249bc4f7015cbe12e72c6081f358e40fde1fc","datavalue":{"value":"5977511","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3100211$E72CDCAB-EBA9-4AB2-A315-F14940C67A8F","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"b48d7b42095141e48a9c1788caedf5498122de8b","datavalue":{"value":{"entity-type":"item","numeric-id":31441,"id":"Q31441"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3100211$D7B4FE32-648C-4FB2-A6F2-0342398083A1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ab6ee58efeeaa685ac2b8ecf828badcfb673e8c7","datavalue":{"value":{"entity-type":"item","numeric-id":12929,"id":"Q12929"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3100211$1A91F89B-CF5B-46C9-B883-A755F7DE0802","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ebe6f223efc2405cf071214b7d4e0e7858bf57fc","datavalue":{"value":{"entity-type":"item","numeric-id":18367,"id":"Q18367"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3100211$8F3CC0ED-6A02-4BD0-86AE-158D7BC07669","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"73bf07fb0985efe0166024eb806e5cf2244671a5","datavalue":{"value":{"entity-type":"item","numeric-id":18489,"id":"Q18489"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3100211$C7DED74A-B0DA-409C-A642-5195C4E5BF3D","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":"Q3100211$4B510050-8588-49BD-B6BA-06FFFEECB55D","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"63d2eda7900e6b2c402c102e52367932da9c72c3","datavalue":{"value":"W2096639003","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3100211$6045AA41-2F26-45C1-8E5C-77FF93492B2E","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"bb15445443b7a8677c7ef043ed8530f20d54b0c3","datavalue":{"value":{"entity-type":"item","numeric-id":3100209,"id":"Q3100209"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3100211$FC4DFB46-F88A-4D6C-BD52-3CB979494567","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"20e8225b7fde56abf09e51400675a474f11c4844","datavalue":{"value":{"entity-type":"item","numeric-id":3612435,"id":"Q3612435"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3100211$62E7853B-5501-431B-BC7B-B84B81D72143","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c1a24cffd41ef373432aa4b100a31bd9fd24151a","datavalue":{"value":{"entity-type":"item","numeric-id":582073,"id":"Q582073"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3100211$7A548EA1-1628-459C-BBE0-D38E36411AF2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"bce4f5ae886a6add198cde1454a758dfcc3c40fe","datavalue":{"value":{"entity-type":"item","numeric-id":3932277,"id":"Q3932277"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3100211$03E2E264-5136-448D-952A-E8316E054328","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"decc60dfbdecb52e4624e62a3849ec2745afa0d5","datavalue":{"value":{"entity-type":"item","numeric-id":5747648,"id":"Q5747648"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3100211$45F2FA68-9E28-444E-8AA5-0327760A1A8B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e39b46036e0e44c388baf61cdcb5ecf5b5fa7252","datavalue":{"value":{"entity-type":"item","numeric-id":4447224,"id":"Q4447224"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3100211$3CF37682-657F-46F5-8178-91C3E3A03E94","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d5dc32522e0062cccf7ff7280961b0c091134e3a","datavalue":{"value":{"entity-type":"item","numeric-id":5901563,"id":"Q5901563"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3100211$5EED39D0-6D21-4476-839F-6FBDEE3C7B48","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0e2b469eaa8f0fd6e966a39a79c085825d6fa8ce","datavalue":{"value":{"entity-type":"item","numeric-id":1598445,"id":"Q1598445"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3100211$B4B7B36B-3510-4F56-8078-803B79C5ABBB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f45e40f028c5051cb72e103b5cc02af7f7932624","datavalue":{"value":{"entity-type":"item","numeric-id":5176973,"id":"Q5176973"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3100211$E79B4F56-D595-4FEF-9A68-C7DC22D6227E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9811e0f445518a60fcf8a88a2ec5cd76d23ab843","datavalue":{"value":{"entity-type":"item","numeric-id":5477649,"id":"Q5477649"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3100211$5F94727E-02CB-4C5B-8441-DF8EA39F3F10","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"084eef17a096b7c40c0fb41db727301ceb159c5b","datavalue":{"value":{"entity-type":"item","numeric-id":1868511,"id":"Q1868511"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3100211$2D182998-07FB-4E4D-82E0-A768D9CB8154","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a5809a6684c365442525c649f10f3cfd46627fcb","datavalue":{"value":{"entity-type":"item","numeric-id":1825045,"id":"Q1825045"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3100211$725D63D1-3269-459E-8EEF-BD6B06092E48","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8670a1cb5138f59a7607a06c6c33e9eef7f2c9ea","datavalue":{"value":{"entity-type":"item","numeric-id":3938536,"id":"Q3938536"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3100211$18CAF30E-A710-4F84-8765-61A9C90D3B1C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"10514d04294539f6b18e653ffed15729ce3e519b","datavalue":{"value":{"entity-type":"item","numeric-id":5678447,"id":"Q5678447"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3100211$21E417A5-FFB1-47D0-96D9-B64D72610DFB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6ff7181965704e473c064c7d95f9f7f0b397f93f","datavalue":{"value":{"entity-type":"item","numeric-id":3543665,"id":"Q3543665"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3100211$E7F195D4-25D8-49C1-9A46-AC727DDE9B11","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"210fc6ea1c74927f8cc30615348c9f5912fd19d2","datavalue":{"value":{"entity-type":"item","numeric-id":3586063,"id":"Q3586063"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"17c29fbeb6f732d175d2217ae6ea43ca3c6b0fa6","datavalue":{"value":{"amount":"+0.89298666","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":"Q3100211$B02985F9-1040-4163-A67E-A6D4A3EE6630","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"793d268335cb0310030c003f9a67cbb04ebc75e9","datavalue":{"value":{"entity-type":"item","numeric-id":5747648,"id":"Q5747648"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d57daa59c14afd53e00dbd8b678b0401004fd5df","datavalue":{"value":{"amount":"+0.8484931","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":"Q3100211$7812225E-9B1D-476A-A677-57D0ABDA4E89","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1813dee6ade6ce3af2af73d2234b94398df48393","datavalue":{"value":{"entity-type":"item","numeric-id":5958299,"id":"Q5958299"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"aa63a70dade11d2b93591bb929e1b961b3758fb6","datavalue":{"value":{"amount":"+0.8465414","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":"Q3100211$5D17F5E7-5CCB-48CE-83B0-6BE248576C33","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5688ed66a44257c423ffa0f6cb24d2c0a8e4433a","datavalue":{"value":{"entity-type":"item","numeric-id":4645754,"id":"Q4645754"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5ae40b8c11e219fc23714c9af370f59e4f0f4235","datavalue":{"value":{"amount":"+0.8442513","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":"Q3100211$AF5AF22F-2037-4F1A-A587-FAFEF35C0F25","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"16c724725837931461cac224b93554ded3c2abc9","datavalue":{"value":{"entity-type":"item","numeric-id":3194730,"id":"Q3194730"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"635a9947e9474db41d9a75f0a4aef98ee936f1d4","datavalue":{"value":{"amount":"+0.84210104","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":"Q3100211$96C6507A-0150-4A17-82CD-F8F7A4C76A0B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c6d150078fa254a20d5b7abef84a8e28474e9671","datavalue":{"value":{"entity-type":"item","numeric-id":683741,"id":"Q683741"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8268427a6a488ad47a10a4aea385204803152458","datavalue":{"value":{"amount":"+0.8405617","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":"Q3100211$2287C0B7-67CB-47AA-BB0C-F027D833FAFA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a7b6d5d9914f2d37077df71dc6315d295973db81","datavalue":{"value":{"entity-type":"item","numeric-id":2829276,"id":"Q2829276"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"626f1052921c72c85cf883dd52fc163ff4d89008","datavalue":{"value":{"amount":"+0.8394895","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":"Q3100211$F1DB7D76-634B-49FA-80CB-B2E8257A1946","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"25a292ffa5a7559f4c25ec891c21f354936540be","datavalue":{"value":{"entity-type":"item","numeric-id":3100210,"id":"Q3100210"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"fbc01c6d908f217455d81b94b80de64fabe1129c","datavalue":{"value":{"amount":"+0.8387599","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":"Q3100211$6E17DD64-6298-4FCE-9F0C-B707E79F17B6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"758f0e559936a3fcd21e65aa9c59b49f3d1a2862","datavalue":{"value":{"entity-type":"item","numeric-id":1791149,"id":"Q1791149"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"412835a6fc48d39599e2bb44c53e063a84125821","datavalue":{"value":{"amount":"+0.8357703","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":"Q3100211$A5CA9D42-B34D-4059-BAC5-E1DB0D1D1DCA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6d22b9f82cd9bd048e12fef8e502f52d443ca7e3","datavalue":{"value":{"entity-type":"item","numeric-id":3586040,"id":"Q3586040"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"49c3f02679fc18066bb6a045492d08aaee680bff","datavalue":{"value":{"amount":"+0.8340249","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":"Q3100211$B7D8698A-9590-44F0-9E9C-C4ACF1E16C9D","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:3100211","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:3100211"}}}}}