{"entities":{"Q7361944":{"pageid":31521371,"ns":120,"title":"Item:Q7361944","lastrevid":105370535,"modified":"2026-10-07T13:39:11Z","type":"item","id":"Q7361944","labels":{"en":{"language":"en","value":"Quantum Hoare Logic"}},"descriptions":{"en":{"language":"en","value":"AFP entry QHLProver"}},"aliases":{},"claims":{"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"5e74402a97a20030488194dd58c983bda4ca8244","datavalue":{"value":"https://isa-afp.org/entries/QHLProver.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q7361944$A595A776-A260-411E-9711-8733025B298C","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"5d99dbe30829bae41f2758b5bf096ee886d2b78f","datavalue":{"value":{"time":"+2019-03-24T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q7361944$CB7CDAF7-A611-4987-830D-AF0F5E7E36B9","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"d410b715db143d709126f7ae197e8a59a835ea37","datavalue":{"value":"Junyi Liu","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361944$F8199AB7-0C52-43BE-9C40-674294E04A84","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"01aade34926865f306029ac4b82b2852e9efa5b5","datavalue":{"value":"Bohua Zhan","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361944$2018B09B-D18B-4A2D-8C7A-5EC4CC7060B7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"178d39f24994d71a0af5248c9933b7152e4cc6c2","datavalue":{"value":"Shuling Wang","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361944$003D8051-E7BF-4155-B5D0-E9ECF9CEDC0A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"2f8bc73a06de083f23430ac39364a385e67e4cf5","datavalue":{"value":"Shenggang Ying","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361944$3DD3F88B-EF1B-4055-A762-AD51404E2BCD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"90772222bf2ce08a44e3e9e295349f0144974751","datavalue":{"value":"Tao Liu","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361944$E20A8081-9EF7-495A-813A-4CF4B929FC58","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"c01daf26b176217f63dc48c581b6fb4637b8f107","datavalue":{"value":"Yangjia Li","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361944$CC37F998-BA26-41AE-83F1-C8B19CBD6C86","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"5ad2a0940e98e7fe4d043548a3e57fc4a53e081c","datavalue":{"value":"Mingsheng Ying","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361944$9D3FE872-7F4F-4DE2-A8FD-A93F38D38444","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"a3a9bd8c0a129420770a9b65b66917d63ded1013","datavalue":{"value":"Naijun Zhan","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361944$3A6E5568-C33C-4943-85C2-7DF608A1D747","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"f67252a09067c4c6897917c86c4478de7557254f","datavalue":{"value":{"text":"Quantum Hoare Logic","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q7361944$7CF77052-484F-4E8E-9B79-80559226BC4A","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"c713262f3600040f51da36ce679f7329cd4c7651","datavalue":{"value":"We formalize quantum Hoare logic as given in [1]. In particular, we specify the syntax and denotational semantics of a simple model of quantum programs. Then, we write down the rules of quantum Hoare logic for partial correctness, and show the soundness and completeness of the resulting proof system. As an application, we verify the correctness of Grover\u2019s algorithm.","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361944$24176D8A-7D74-4495-8569-FA36EB63C299","rank":"normal"}],"P37":[{"mainsnak":{"snaktype":"value","property":"P37","hash":"9a21a8eebe97539644aa32b24dda137c12e751dc","datavalue":{"value":{"entity-type":"item","numeric-id":40327,"id":"Q40327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361944$1757018C-4AAA-4089-BC57-9DB6C940D4FE","rank":"normal"}],"P585":[{"mainsnak":{"snaktype":"value","property":"P585","hash":"d5e8fc5aec7dde11f4c13854060e8aa8aa89e92b","datavalue":{"value":{"entity-type":"item","numeric-id":7361091,"id":"Q7361091"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361944$6156126C-D60E-4407-8BC4-BF65E6316A24","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P585","hash":"67e8a5ea879a7dc06c8ce830c1b61b9bb35cc48f","datavalue":{"value":{"entity-type":"item","numeric-id":7361432,"id":"Q7361432"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361944$E9C1411F-3133-42FF-BAC2-ACEF52E932A0","rank":"normal"}],"P2651":[{"mainsnak":{"snaktype":"value","property":"P2651","hash":"aa8f6bd5a2b4440f838b34acf103bdf45fee4f56","datavalue":{"value":{"entity-type":"item","numeric-id":7360797,"id":"Q7360797"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361944$6CDD271E-94F0-49E7-862E-26FD68C87900","rank":"normal"}],"P1460":[{"mainsnak":{"snaktype":"value","property":"P1460","hash":"908c3454b3659c4b140ccce33c5aee31081edc8d","datavalue":{"value":{"entity-type":"item","numeric-id":5976450,"id":"Q5976450"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361944$69791E63-4D34-4A1C-BA8F-773956FAE689","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Quantum Hoare Logic","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Quantum_Hoare_Logic"}}}}}