{"entities":{"Q2914237":{"pageid":2924957,"ns":120,"title":"Item:Q2914237","lastrevid":42492984,"modified":"2025-06-30T10:04:16Z","type":"item","id":"Q2914237","labels":{"en":{"language":"en","value":"Canonized rewriting and ground AC completion modulo Shostak theories: design and implementation"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6086014"}},"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":"Q2914237$DF0AADA3-2BC1-455E-A848-39EEB814C840","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"353f598d68d2fe7d21ba010cfec02e276298768a","datavalue":{"value":"1253.68291","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2914237$60B684C6-07ED-4F6C-96EB-0AD5DA1A3B0B","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"8412d59b06f7cc474761f1a220493a6bc87cc951","datavalue":{"value":"10.2168/LMCS-8(3:16)2012","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2914237$52FFCEFA-8736-491B-8B55-14472138F9B6","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"2a9c3e977eb61b9fc5b2fcb92fe6e8ddc0a12670","datavalue":{"value":{"entity-type":"item","numeric-id":287381,"id":"Q287381"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2914237$86A2858C-5CA5-41C1-A209-C843D3EF61DF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"55727f9f4a7efb137e6c3bf39c513ca15ab9ea55","datavalue":{"value":{"entity-type":"item","numeric-id":851140,"id":"Q851140"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2914237$0E83352D-D429-4EE9-9A5D-C1512BA7BF06","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"eda4e24824b9a053142e8e90e1770228f6ccf88f","datavalue":{"value":{"entity-type":"item","numeric-id":2908478,"id":"Q2908478"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2914237$5A3EA716-0952-4E3D-A105-517ED263E2FB","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"da58c52dc46c86e7440f2499c9e1bef3537c5562","datavalue":{"value":{"entity-type":"item","numeric-id":2786118,"id":"Q2786118"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2914237$510AB7AA-D2F3-4DD7-AC0A-9AB04F21E81C","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"e6b00aac43a8308ba24a0697ff1b19387c2c0656","datavalue":{"value":{"time":"+2012-09-25T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2914237$AD4D5B5C-703E-4EEE-97E7-40A3ED6874A1","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2914237$764FDEC5-911F-4835-B7DC-71063EFD58A2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2914237$CE9B1736-FD47-45C3-ABA4-732CE43264E9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"c636094cc8b933189eabd7c009d327f829bc6ac4","datavalue":{"value":"68Q42","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2914237$45CD2CF6-CAB6-4CD9-BE34-F6512446A907","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"1846d95b5e8ea827e9c5e5ce691d836f9a85fa37","datavalue":{"value":"6086014","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2914237$6307A39C-A63F-4599-B905-DCB5DD7E3C57","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"eb79299daf8f29391d6c8a2b4222865ffe474551","datavalue":{"value":"decision procedure","type":"string"},"datatype":"string"},"type":"statement","id":"Q2914237$2D851AE0-5475-49D7-B175-AD27B09B510E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a7a05fe3fe593893a51a65c1460f04fadb15973b","datavalue":{"value":"associativity and commutativity","type":"string"},"datatype":"string"},"type":"statement","id":"Q2914237$C34CA588-5584-447E-93C6-6204D589AD48","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"476e70cc5d552d5cdc76575cc73d40a8bfb4b86e","datavalue":{"value":"rewriting","type":"string"},"datatype":"string"},"type":"statement","id":"Q2914237$ACA5C505-11EA-4A75-A006-747371B8F2FD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"8fb1ffbf0e110d34e5822023c4d3be048bbe68ae","datavalue":{"value":"AC-completion","type":"string"},"datatype":"string"},"type":"statement","id":"Q2914237$3958D982-0AB5-4759-BC23-A1AA225D6B6E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"61439d791f6aac729372268f16b553bcf47e3b78","datavalue":{"value":"SMT solvers","type":"string"},"datatype":"string"},"type":"statement","id":"Q2914237$DAC9C8E0-3878-45F7-95CB-C3E44FE3C460","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"deb62032a682d181e06499e81b0f01b8d84a7498","datavalue":{"value":"Shostak's algorithm","type":"string"},"datatype":"string"},"type":"statement","id":"Q2914237$3CD9DFA6-DEF1-4E2B-8A63-783A4511187E","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"72973e2f3c2b37eaccccd6859e905abdf48d99e4","datavalue":{"value":{"entity-type":"item","numeric-id":17040,"id":"Q17040"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2914237$8E0AC3A5-5EC0-427D-AC53-966FC2992920","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":"Q2914237$7EA2294B-E7C5-4AFD-8D1E-86353A6189F8","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"ce05909f0c64552a93f6fd411d68eed4ee33a4c2","datavalue":{"value":"https://doi.org/10.2168/lmcs-8(3:16)2012","type":"string"},"datatype":"url"},"type":"statement","id":"Q2914237$09307286-DF0C-4399-B123-114D274455C5","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"e6f953b45919df11b4f0c7b1e7544e1a42331534","datavalue":{"value":"W3101473842","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2914237$CEFA1B47-9FF0-44DC-9046-8ADB31C36BC9","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3ad08e0efaa5023d710d3d27ad3418bf02b424fe","datavalue":{"value":{"entity-type":"item","numeric-id":3000635,"id":"Q3000635"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4793a09fcaa806ef7dfe5ab1210e3059a1de25fa","datavalue":{"value":{"amount":"+0.98414445","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":"Q2914237$DA60B171-AB28-4A85-992A-7EF80FDDAA8A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6997b5678308a20a1e5e81827d70db9d4424ca51","datavalue":{"value":{"entity-type":"item","numeric-id":2842873,"id":"Q2842873"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6ef4a0b433c7c9be57d45e4e32b8d1c8c0c99403","datavalue":{"value":{"amount":"+0.8550677","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":"Q2914237$E560CB3A-2B49-4A00-BDB5-551FDC98B289","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8f5a42e658543452fe32c23cfa6bc53fd395c5ba","datavalue":{"value":{"entity-type":"item","numeric-id":5055849,"id":"Q5055849"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"79f603d4886a2fc2d74123ba200ec1200a7cc01e","datavalue":{"value":{"amount":"+0.85373944","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":"Q2914237$6DA266DE-AC57-4FD9-A929-A33636BA8041","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7584b082b37b4d35c9ebaef5f02795ec22876e3f","datavalue":{"value":{"entity-type":"item","numeric-id":2291817,"id":"Q2291817"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"49f02024a12932465f56c766802c7c7a479afdf1","datavalue":{"value":{"amount":"+0.852345","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":"Q2914237$184E22CE-DA2C-46FD-A7EC-BF1C9B3E6D86","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e9271f3ed2dd88ca444b08be6f941aa5d79de17c","datavalue":{"value":{"entity-type":"item","numeric-id":5739456,"id":"Q5739456"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6d0759c846b42e78310c2eda5caaec5232e9622f","datavalue":{"value":{"amount":"+0.85224164","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":"Q2914237$D2D93FD1-C92B-4F80-A6BD-01ECE1D65B35","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1e9593a334cba750445600d20c97c43b8c00307b","datavalue":{"value":{"entity-type":"item","numeric-id":6164539,"id":"Q6164539"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8871aaa458600f699656aa7edb51003ef808dee5","datavalue":{"value":{"amount":"+0.85079914","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":"Q2914237$C55358EF-7618-49BA-9DA8-31C5A95522C2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7f72e67ffb8794611707ce233a5e778fa44d33a2","datavalue":{"value":{"entity-type":"item","numeric-id":1350349,"id":"Q1350349"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5b1ccb29834593877e170b7612f6ddde445fa44f","datavalue":{"value":{"amount":"+0.84840685","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":"Q2914237$8C94E153-308B-4398-AA76-EAB76BF7C6BC","rank":"normal"},{"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":"ae0d68f8d50c1eca7d87b56a14967005450ff762","datavalue":{"value":{"amount":"+0.84736013","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":"Q2914237$7E346333-A903-4D79-81E3-1F4C61DCA3FC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"aae04451bba5241f6a0672ec38a6617f41caa3ac","datavalue":{"value":{"entity-type":"item","numeric-id":4594224,"id":"Q4594224"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c87ce49958e3733420eac0791029c548368377be","datavalue":{"value":{"amount":"+0.8432809","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":"Q2914237$3BC8733D-C36D-4C8D-B766-70CDAEC0A3CE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"cd13546199e36837498d0f86201f321fdd87908b","datavalue":{"value":{"entity-type":"item","numeric-id":5941752,"id":"Q5941752"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a7b48023df7d08e2b470a3514cd63b6192ef2123","datavalue":{"value":{"amount":"+0.84310466","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":"Q2914237$06755717-DF21-4968-8602-040484306C0A","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"d03628904f29584909fa70afe3442c5239d62b12","datavalue":{"value":{"text":"Canonized rewriting and ground AC completion modulo Shostak theories: design and implementation","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2914237$62836203-94E7-47C1-9909-FAF1203230C4","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:2914237","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:2914237"}}}}}