{"entities":{"Q540690":{"pageid":542457,"ns":120,"title":"Item:Q540690","lastrevid":51261260,"modified":"2026-01-17T12:16:17Z","type":"item","id":"Q540690","labels":{"en":{"language":"en","value":"The right tools for the job: correctness of cone of influence reduction proved using ACL2 and HOL4"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5903837"}},"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":"Q540690$1B2A8F43-E6BA-4C88-A404-03E2D496F1D6","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"46d749b60d34bbe2067f9fad9e33ad6fcc4a6692","datavalue":{"value":{"text":"The right tools for the job: correctness of cone of influence reduction proved using ACL2 and HOL4","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q540690$9914A7BA-F3C3-4458-A364-DB41CA17A40E","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"291fb61529d062cd2c37f805a84ff5704b74db78","datavalue":{"value":"1216.68233","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q540690$9F70084A-90C5-452A-8B10-312D298EB852","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"931e30a40c8472ba029c509504f463b9cccdfd3d","datavalue":{"value":{"entity-type":"item","numeric-id":436371,"id":"Q436371"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q540690$83FDFF4B-10BD-4F2E-8270-B2D669FCB5D4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"e6bbab2ea230ef82cf7d72bee404dd827d5aaeed","datavalue":{"value":{"entity-type":"item","numeric-id":230814,"id":"Q230814"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q540690$E5714139-0966-406D-8447-194FDE62B1EF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"f5a9bcb5f8b5c271cc4d9ccff897b2db1a111ede","datavalue":{"value":{"entity-type":"item","numeric-id":540689,"id":"Q540689"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q540690$7D4B7D23-D8A1-45B0-9348-A217B6751786","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"b84cc8b5923f45dc86ae69f67f68bf56d7ecfce9","datavalue":{"value":{"entity-type":"item","numeric-id":174771,"id":"Q174771"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q540690$3DBAE880-47B9-4787-BE1B-162D95B25E39","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"97ec2afdf79c6632e29986375b104998c12b878d","datavalue":{"value":{"time":"+2011-06-03T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q540690$788EAFB9-73D5-47B8-859C-C0377CF455AE","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q540690$9FA4179A-B4BB-451E-BA1C-8F6D77C63A7C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e2244b32b83bf71a9c045223e635ab074452b389","datavalue":{"value":"03B44","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q540690$1458283D-DB24-4EDC-AAD9-D8542944560A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q540690$9160F0EE-53CE-4B2B-9E84-EC820F088D76","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"7c954a057a2b5eae2c9e99bb56abe4f2362613ad","datavalue":{"value":"5903837","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q540690$34296426-75BC-4742-BC83-70B67F782ACE","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"22498cf86e242a38d9fe355523225aa55193233b","datavalue":{"value":"theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q540690$B4F3F3CC-3D30-4872-89FA-A123F2307029","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1ca1042868ff4f694776e4b2c62ec66638c4ef91","datavalue":{"value":"automated reasoning","type":"string"},"datatype":"string"},"type":"statement","id":"Q540690$08A75F93-FB1A-415D-8992-1F86CD0D2AE5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"39810ec381ba48fb5861c168391fa7d328efd8b1","datavalue":{"value":"higher-order logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q540690$4CE5DF82-3FC8-4CB2-8A5E-5F4C65E00B82","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"0a3a42aadcbf55cfbbe59444027d87b65e905d6c","datavalue":{"value":"combining theorem provers","type":"string"},"datatype":"string"},"type":"statement","id":"Q540690$63A6E269-907E-4C4F-9458-81B41CC1DB55","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1f1cf12c900aeb5813ce8f84db8812e6bb27ae87","datavalue":{"value":"linear temporal logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q540690$0D049C66-87F1-4FE3-9A65-BD647F6FA64A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"fb9f8004d477a3922fe8bde53d670f8b57c48852","datavalue":{"value":"model checking","type":"string"},"datatype":"string"},"type":"statement","id":"Q540690$5F20DED5-865A-49CE-8F43-50F0034E6F57","rank":"normal"}],"P1463":[{"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":"Q540690$2D3ADF9C-B3B0-44A9-A0FE-ED00F8B69315","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"53a4a9b6c38d395d5b2eb80cedc3eefcbf3e9947","datavalue":{"value":{"entity-type":"item","numeric-id":15987,"id":"Q15987"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q540690$B446514C-8E95-46A6-9EDE-EC558F2BBBE0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"7f231912461a4cf859d87b4356c5e2a2037e1e84","datavalue":{"value":{"entity-type":"item","numeric-id":17631,"id":"Q17631"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q540690$2F5E541C-781B-4D06-B7AF-BFB9D051B628","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"2b02b46847f3d7e3a5825b9484a88607b98dbd14","datavalue":{"value":{"entity-type":"item","numeric-id":13958,"id":"Q13958"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q540690$287C36D5-DBAD-4AFC-AD39-64C00AF0E49C","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":"Q540690$72B82A67-7FFC-41C0-814B-C1A28916D514","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"76bed64f69e1e54eff331855100d58acb125f75f","datavalue":{"value":"https://doi.org/10.1007/s10817-010-9169-y","type":"string"},"datatype":"url"},"type":"statement","id":"Q540690$05118761-2C24-4DE9-9365-D3E71D555AA9","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"5f7971e0f5dd86bdfbeea3fd8c94cc327fcfe9c4","datavalue":{"value":"W2003674078","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q540690$C3033993-713D-45CA-96FE-5E42B521D854","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"df6d745c28f41f3f6887e89cc1ca892988e70309","datavalue":{"value":{"entity-type":"item","numeric-id":5287513,"id":"Q5287513"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q540690$E0F61D98-1532-4209-9093-9EC6917A03C4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a693c10013eb7bffb7ffbc0c1890644cc6a21fe5","datavalue":{"value":{"entity-type":"item","numeric-id":4809048,"id":"Q4809048"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q540690$EEBB7D9E-C15E-4B78-87A5-36DF7A9A6606","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"672be30d9c0fd1bb08a1fc6131d1506ec245277a","datavalue":{"value":{"entity-type":"item","numeric-id":4830107,"id":"Q4830107"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q540690$BBD71AE2-47F9-4446-B411-32E0DF4C5E96","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ca6926d9a2864657c63c8ba6d81f03198b036942","datavalue":{"value":{"entity-type":"item","numeric-id":1595929,"id":"Q1595929"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q540690$26A7F625-62F1-43D5-9A51-7B1020FA31AA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ffe62377108373cd046811a24014b149bc79d51e","datavalue":{"value":{"entity-type":"item","numeric-id":3543644,"id":"Q3543644"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q540690$A18D6604-7F84-468B-9E10-2004F63A48C2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3f60db55428521e0cf5ccdeaa2bf5e3fd0ed1e94","datavalue":{"value":{"entity-type":"item","numeric-id":4326390,"id":"Q4326390"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q540690$95D0EA5A-754F-42DE-B93B-9FDAF8A576BA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"412697b27bc0e191017d5a3e9cbfafa45de8e608","datavalue":{"value":{"entity-type":"item","numeric-id":2566223,"id":"Q2566223"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q540690$023A749E-8C9A-4AE2-92AB-5BDDC8B820C8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"77f4334b25d43b9293350a877e2d317280ca55a9","datavalue":{"value":{"entity-type":"item","numeric-id":3543646,"id":"Q3543646"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q540690$CEDD14A9-3C67-423A-A053-C84C3FAA30D3","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"a9f305b9b3bd49eabfa5c4ec87af37b4d7102f7a","datavalue":{"value":"10.1007/S10817-010-9169-Y","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q540690$6BEFEEFC-53B4-4352-B412-3677817A0540","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"067b9ee5d1759bf8dfdf5a7d76851fcc9c0894c5","datavalue":{"value":{"entity-type":"item","numeric-id":1610218,"id":"Q1610218"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"fada50f553f03e01bc56698f740bdb872261cb4f","datavalue":{"value":{"amount":"+0.7095224857330322","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q540690$AC9A73D2-FF97-4D49-A31E-493E1F523026","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7db5f6f879711fee2556071b86a425c26dd16b51","datavalue":{"value":{"entity-type":"item","numeric-id":3523181,"id":"Q3523181"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6b39ab6d07107cf8cbe4f1261e29ebe7ad2c4bc9","datavalue":{"value":{"amount":"+0.7011427283287048","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q540690$7C82DCDB-A03F-43FB-8CA5-4A3E87968386","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"efd8dc0e0b76d191fd26f35e8e5741833044fd26","datavalue":{"value":{"entity-type":"item","numeric-id":3543646,"id":"Q3543646"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8a4c08dc1dcc68a4b86c076ab01662f519d8cae7","datavalue":{"value":{"amount":"+0.7009387612342834","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q540690$1B77DA03-7CBB-4DEC-BE1C-BE3D87D368B4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"63e348351fc0d55da2a66fc3a8fea950fad5013e","datavalue":{"value":{"entity-type":"item","numeric-id":2848688,"id":"Q2848688"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6498823146cc10b82ddf1dd30f5f118df442e5f0","datavalue":{"value":{"amount":"+0.7005388736724854","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q540690$CAB80499-69BD-4E01-9543-F195BD26124F","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":"d5610e013214b1931f8ddf504d61288fa565fff5","datavalue":{"value":{"amount":"+0.6924504637718201","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q540690$40ACA399-329A-4E11-A663-639DC2187397","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:540690","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:540690"}}}}}