이 논문은 만족 기반 양자 Hoare 논리의 상대적 완전성을 증명하였다. 이를 위해 먼저 결정론적 단언과 양자 프로그램으로 구성된 Hoare 삼중체의 의미론과 증명 시스템을 수립하였다. 그리고 결정론적 단언의 최약 선행 조건을 활용하여 확률적 표현의 최약 선행 용어 계산을 구축하였다. 이를 통해 양자 Hoare 논리의 상대적 완전성을 도출하였다.
