{"entities":{"Q2164216":{"pageid":2174959,"ns":120,"title":"Item:Q2164216","lastrevid":82570475,"modified":"2026-05-06T21:13:13Z","type":"item","id":"Q2164216","labels":{"en":{"language":"en","value":"SMTCoq: a plug-in for integrating SMT solvers into Coq"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7571373"}},"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":"Q2164216$A8EBAA01-5B12-4CE3-AF42-73170BEE1202","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"a59ee293dbbb1175a546138355df03c38bd804a4","datavalue":{"value":{"text":"SMTCoq: a plug-in for integrating SMT solvers into Coq","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2164216$CE9185BD-F3D0-4EA1-833B-369BC8658670","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"dbb5caf3502e541d10775ba91eb415df762d7d8e","datavalue":{"value":"1494.68285","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2164216$ABE2A142-CE5E-4F0E-B875-3BC60D2A7A15","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"26670311f9be45235ffc67e9a09217a167a01dcd","datavalue":{"value":"10.1007/978-3-319-63390-9_7","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2164216$8DBE3C1A-80D7-4959-98C9-629F757B301F","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"23de4e42d26c5ff113394f059a29a12c73855bdd","datavalue":{"value":{"entity-type":"item","numeric-id":1798945,"id":"Q1798945"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2164216$852BE9B9-5E62-4833-B759-0F3E6F44DE33","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"b3845063a240ec80df9eff0093d13cd3b4659df0","datavalue":{"value":{"entity-type":"item","numeric-id":2164215,"id":"Q2164215"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2164216$026C8173-9D31-476A-8A01-A069701D3649","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"947e5398223830d4c80e75386dbd3c8e6dd67f1d","datavalue":{"value":{"entity-type":"item","numeric-id":429585,"id":"Q429585"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2164216$F7C7B799-AF97-4E38-A779-651998328A0D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"b6e50206a6040e5309045ac8ce1bd781dc58d9c2","datavalue":{"value":{"entity-type":"item","numeric-id":1683462,"id":"Q1683462"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2164216$F7A4749D-566B-4DAF-B870-237CE680DBF8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"051db72c27a6ffd1dc64c69febb1b92cb862178b","datavalue":{"value":{"entity-type":"item","numeric-id":2151236,"id":"Q2151236"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2164216$5718AECD-75C1-43C8-957F-539DE0E3C0A1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"84952d23570c02a49b2cbd6b6731071617699380","datavalue":{"value":{"entity-type":"item","numeric-id":518398,"id":"Q518398"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2164216$E4B63BF8-2BEB-46F4-8BF5-029CBC3B31D3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"ad77f9f95b13763d1bf3e18f3ef5b6900b795f74","datavalue":{"value":{"entity-type":"item","numeric-id":518400,"id":"Q518400"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2164216$571AC276-BA3F-4196-A271-C8AC71E8F86C","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"7aa7040e0858a957251ee78ad1edc7d13d61d833","datavalue":{"value":{"time":"+2022-08-12T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2164216$93AC6DEC-9964-4386-935E-79E5AFF8B053","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2164216$7185EA28-C131-4506-AB9C-BD0C0CCE80A0","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"0d33fb5e248316ec404ffe8f46fbb7814cc698af","datavalue":{"value":"7571373","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2164216$B803D4BC-607D-411D-9C7F-7E02ED0C4FC4","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1254a7c01d2970b87da2854c1fde40c268a1f55d","datavalue":{"value":"satisfiability modulo theories","type":"string"},"datatype":"string"},"type":"statement","id":"Q2164216$41AD7D68-13D9-4412-B9D0-18B11968583C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"96c637bd04eeadc0d155dfc114a8e790a3102174","datavalue":{"value":"proof certificates","type":"string"},"datatype":"string"},"type":"statement","id":"Q2164216$76E4C6BC-42EA-43F5-9ABF-9DFEC26C80F2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"6385ef27793b04b6a19affe021092f56d6415acf","datavalue":{"value":"ZChaff","type":"string"},"datatype":"string"},"type":"statement","id":"Q2164216$B9025FF5-EE74-4915-BF9B-9E58650E23E9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"0dea93a4bcfcef392a315733cc6349528152d45f","datavalue":{"value":"external solvent","type":"string"},"datatype":"string"},"type":"statement","id":"Q2164216$4E9E3676-9DB7-407B-92DD-8E1BCDF5DE68","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"b12b08449d5103681493833fde815e542a05327e","datavalue":{"value":"functional arrays","type":"string"},"datatype":"string"},"type":"statement","id":"Q2164216$75C4804B-B28F-475C-8D8E-B1378B8B0A1A","rank":"normal"}],"P1463":[{"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":"Q2164216$1E99489C-8458-4DD8-8FAC-422C7E43A0B1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"5b9460a01ea60cde385cddccbe3b63d66f761f84","datavalue":{"value":{"entity-type":"item","numeric-id":44021,"id":"Q44021"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2164216$57E117DD-3AE7-445D-AFAF-13C8471FCDAE","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":"Q2164216$D9EE3172-2ED3-47B7-96DB-AFF54D060B51","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"10bba3d2c709c6a89cfbeec59bcf5e8a91bb862d","datavalue":{"value":"https://doi.org/10.1007/978-3-319-63390-9_7","type":"string"},"datatype":"url"},"type":"statement","id":"Q2164216$D4424E80-EE47-40C1-BBE2-22D46ECC32DC","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"78474f5068329a486b3def395deaf516812fca5a","datavalue":{"value":"W2735882127","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2164216$1C3964A7-4A9D-42E6-B569-DC65F015FC5B","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"fa0c8580ce4e0cb685d0ff86138835bcfa17cf41","datavalue":{"value":{"entity-type":"item","numeric-id":3100209,"id":"Q3100209"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"71144c82fdaaef0d749600ec31dae43d3694dd85","datavalue":{"value":{"amount":"+0.90330654","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2164216$493C248B-612A-429B-84EE-09D7BE775E2C","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":"838c58155946363a1248b44aab79904d5462b16e","datavalue":{"value":{"amount":"+0.86889863","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2164216$D440EC6A-052A-4D51-94E4-54752E2A4F12","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a2736b661563708670c0260aac3786ab930b183d","datavalue":{"value":{"entity-type":"item","numeric-id":2360873,"id":"Q2360873"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"cb5f94a31a2c2db49cfb7c894990253c49e6d1f9","datavalue":{"value":{"amount":"+0.8549543","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2164216$A2D3F311-9B49-46DD-8D73-CA3ADD03DA8E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1b5192e189433aa3c67746a2f4880b6830d9d2b3","datavalue":{"value":{"entity-type":"item","numeric-id":3454092,"id":"Q3454092"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"cb5f94a31a2c2db49cfb7c894990253c49e6d1f9","datavalue":{"value":{"amount":"+0.8549543","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2164216$197711BF-8271-4F87-ACA6-22FA0D62D644","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ce890fe61354b539d058e92db345c05932c2b22b","datavalue":{"value":{"entity-type":"item","numeric-id":2118327,"id":"Q2118327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"bb542558226f6f1a4bc632f416288aa3b5d5718a","datavalue":{"value":{"amount":"+0.8495108","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2164216$D1183D36-32FA-4930-8351-11BABFD255FE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d943961f845ca0e5235cda46d1b02c9a1ce4d34f","datavalue":{"value":{"entity-type":"item","numeric-id":5747643,"id":"Q5747643"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"867fa22067b63b6050279a4f6d7b841186098373","datavalue":{"value":{"amount":"+0.836972","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2164216$A70187B1-D074-46B8-BF4F-19231D893B2B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4e42c0696ebfd3fb16c17afdd0eec4ae5147edf7","datavalue":{"value":{"entity-type":"item","numeric-id":5200019,"id":"Q5200019"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5afd09adaecdf20c6c188f56d1d9a24f521eee75","datavalue":{"value":{"amount":"+0.8359704","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2164216$6AA42132-AE06-4107-8C89-90DB40E27236","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e434c6f686246887cde238823958ad79571304c4","datavalue":{"value":{"entity-type":"item","numeric-id":2351158,"id":"Q2351158"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5afd09adaecdf20c6c188f56d1d9a24f521eee75","datavalue":{"value":{"amount":"+0.8359704","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2164216$FA0A6743-28F9-48D1-A15C-3940ED805943","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"SMTCoq: a plug-in for integrating SMT solvers into Coq","badges":[]}}}}}