{"entities":{"Q5747643":{"pageid":7777194,"ns":120,"title":"Item:Q5747643","lastrevid":41573005,"modified":"2025-05-06T00:12:49Z","type":"item","id":"Q5747643","labels":{"en":{"language":"en","value":"Extending Coq with Imperative Features and Its Application to SAT Verification"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5785336"}},"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":"Q5747643$BCD6678A-4467-4311-8C76-C461F4330B5D","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"2114c5d68368f2cf6358a5e46b55dcc41b3b5cdf","datavalue":{"value":{"text":"Extending Coq with Imperative Features and Its Application to SAT Verification","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5747643$E296FB1A-2DC5-4012-AFC0-677FF9974CBA","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"79d482ade4e5f44fce3083d12e0348c2a8d5a88c","datavalue":{"value":"1291.68318","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5747643$31091C39-DF46-45AD-984B-2178549FDB32","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"ffd99364550ef2273d927f8fe8913f3fb5919bcf","datavalue":{"value":"10.1007/978-3-642-14052-5_8","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5747643$36DB2259-0A38-477B-8150-83497639293D","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"6a59fdf2129c99b284ded6d66c20a102c2144679","datavalue":{"value":{"entity-type":"item","numeric-id":3100208,"id":"Q3100208"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5747643$6FFFAB96-1182-46D5-B6F0-B24EF5445CB5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"9bffd823543cff1e715d11a4bf716725d42966bb","datavalue":{"value":{"entity-type":"item","numeric-id":633301,"id":"Q633301"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5747643$83400B1F-D62D-4910-A2C6-CC61B0AD0EFF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"ef3ce062a3abe34fbc66f2165f0b82461a1fec7d","datavalue":{"value":{"entity-type":"item","numeric-id":930884,"id":"Q930884"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5747643$5EF6CB01-45E1-42BC-BDA3-8D868377FFDD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"a5fa5da603477bed196262dce34c616a0a67c991","datavalue":{"value":{"entity-type":"item","numeric-id":742366,"id":"Q742366"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5747643$E08CC2BD-FA8D-48FF-A4EB-4FE648BC2860","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"d43c6ce6e92d67a2cb7e4a7df2a7d5eeec36e724","datavalue":{"value":{"entity-type":"item","numeric-id":2829237,"id":"Q2829237"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5747643$6EE4D073-3D21-4A70-B435-DC85AC73895D","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"5f7d3744053f89b932df935693d4d726597e5f91","datavalue":{"value":{"time":"+2010-09-14T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5747643$5D22B5EF-DE9C-432F-8C12-DBB91251E407","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"d820b342e30a2e50c82d9ad974408ba0cc7b8e81","datavalue":{"value":"https://hal.inria.fr/inria-00502496v2/file/fastcoq.pdf","type":"string"},"datatype":"url"},"type":"statement","id":"Q5747643$C647BCAF-C22A-4AA6-B409-70D53E162C90","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5747643$93E1943E-118B-4926-85D8-717EB628E530","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5747643$DA8B1D5B-8568-4B6E-BCDA-DD49C961FBBA","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"8591df791c5f978f6187da234293c01896ec08cd","datavalue":{"value":"5785336","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5747643$7095499E-4480-4E60-BAB6-9FA08E486CF8","rank":"normal"}],"P1463":[{"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":"Q5747643$F80337F5-8881-42DC-92C3-61A7C841BB5F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"fa5dc13872ba1592e71dabc4befba1daea72a8a3","datavalue":{"value":{"entity-type":"item","numeric-id":14275,"id":"Q14275"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5747643$06820F86-E323-4569-B387-C43670E198D0","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":"Q5747643$A4947645-D86B-4D45-A7EA-65DCA7D344F3","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":"Q5747643$2582FB73-6DFC-417B-A2F1-C7D79B709852","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"d650a7af9fdbfa854d490255d18c32cbaf84928c","datavalue":{"value":{"entity-type":"item","numeric-id":16925,"id":"Q16925"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5747643$C95F6D0E-798E-4729-9996-C41C356FBBCA","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":"Q5747643$728F1BA6-9B00-4BB2-86CD-A3F83A0357AC","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"536c3d03c0dc31bbac861df03d0fe9c8ced51b9b","datavalue":{"value":"W1795725592","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5747643$7E97D525-A268-4870-A0EB-35D0D7271528","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":"9815c19dd22b7e0fe188ee120e4dd8e2636b939b","datavalue":{"value":{"amount":"+0.90372705","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":"Q5747643$743E2127-A60F-421A-BFEB-3594D8150930","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"dc34beb55dbba749ab13c98b095af348386a3fad","datavalue":{"value":{"entity-type":"item","numeric-id":1791188,"id":"Q1791188"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"db3ade382e093b88e05d341229f7b8e1018473e3","datavalue":{"value":{"amount":"+0.8903986","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":"Q5747643$903A2739-BDD4-4A39-A340-37DC2D145F63","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"85fe0cfba50ab81867fa509e16f2465ae8978f99","datavalue":{"value":{"entity-type":"item","numeric-id":4484330,"id":"Q4484330"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"88f8b2684490077060c4f77979f46cdece80d4c5","datavalue":{"value":{"amount":"+0.8740419","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":"Q5747643$4922E6D4-13E3-490D-A49D-8DE9376D9AC2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"54945991e72c4e075bbdaee9b84ef77985d61019","datavalue":{"value":{"entity-type":"item","numeric-id":3087993,"id":"Q3087993"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"42faea3d9727df3beed600dce24ee650d3bafb33","datavalue":{"value":{"amount":"+0.8737737","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":"Q5747643$2BA2B176-62B1-492C-9740-946A73D28FF1","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":"56fb1f402edef350807c82c94e53e738ea6973b1","datavalue":{"value":{"amount":"+0.868744","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":"Q5747643$DF4ED372-05E3-460B-97F7-573826DDEC70","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"51ef567ae3caa4523626ccbb32fa2c077018c262","datavalue":{"value":{"entity-type":"item","numeric-id":2848941,"id":"Q2848941"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7ba329327b16c5654b67b5b1ed8cb96159e425d3","datavalue":{"value":{"amount":"+0.86485106","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":"Q5747643$22CAAAB7-E0B4-4018-AB26-0896EEC0215C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ac9c2eb9482b783c69c8f44330e38517e321c0e7","datavalue":{"value":{"entity-type":"item","numeric-id":4246942,"id":"Q4246942"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5bae1db5f9fb8952c737242a4685a77cfc1a58d8","datavalue":{"value":{"amount":"+0.86271083","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":"Q5747643$09E4E268-EF8B-495E-A71D-A1337BEC2E40","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"36258116623966e4f90ed7ba6a441e7310ba87bc","datavalue":{"value":{"entity-type":"item","numeric-id":2152300,"id":"Q2152300"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"46b2ddb49676b7599e52a2a4bf5dcb46667d2eff","datavalue":{"value":{"amount":"+0.86211884","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":"Q5747643$A3007E39-C072-4CCC-BD5A-4AFD1CA5B601","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7c1b14ec371401427672b91fc35789315ae30462","datavalue":{"value":{"entity-type":"item","numeric-id":2871836,"id":"Q2871836"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"bddfe7a1e16e344e2582d07e2029355bcd6fd4ce","datavalue":{"value":{"amount":"+0.8616377","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":"Q5747643$C793B12E-6212-4BAC-85F6-044AFABB237F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e26c3ee28b2edb7374449f2f1032135d4fba7d2a","datavalue":{"value":{"entity-type":"item","numeric-id":2798255,"id":"Q2798255"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7aa55a16109f04dc354f4a6900024b0d330e9b75","datavalue":{"value":{"amount":"+0.8615559","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":"Q5747643$28EE887F-9563-4F59-B012-BC26746BF656","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:5747643","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:5747643"}}}}}