English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

A first-order logic with quantum variables is needed as an assertion languagefor specifying and reasoning about various properties (e.g. correctness) ofquantum programs. Surprisingly, such a logic is missing in the literature, andthe existing first-order Birkhoff-von Neumann quantum logic deals with onlyclassical variables and quantifications over them. In this paper, we fill inthis gap by introducing a first-order extension of Birkhoff-von Neumann quantumlogic with universal and existential quantifiers over quantum variables.Examples are presented to show our logic is particularly suitable forspecifying some important properties studied in quantum computation and quantuminformation. We further incorporate this logic into quantum Hoare logic as anassertion logic so that it can play a role similar to that of first-order logicfor classical Hoare logic and BI-logic for separation logic. In particular, weshow how it can be used to define and derive quantum generalisations of someadaptation rules that have been applied to significantly simplify verificationof classical programs. It is expected that the assertion logic defined in thispaper - first-order quantum logic with quantum variables - can be combined withvarious quantum program logics to serve as a solid logical foundation uponwhich verification tools can be built using proof assistants such as Coq andIsabelle/HOL.

Birkhoff-von Neumann Quantum Logic as an Assertion Language for Quantum Programs