A Classical Propositional Logic for Reasoning About Reversible Logic Circuits

Holger Bock Axelsen, Robert Glück, Robin Kaarsgaard

Publikation: Kapitel i bog/rapport/konference-proceedingKonferencebidrag i proceedingsForskningpeer review


We propose a syntactic representation of reversible logic circuits in their entirety, based on Feynman’s control interpretation of Toffoli’s reversible gate set. A pair of interacting proof calculi for reasoning about these circuits is presented, based on classical propositional logic and monoidal structure, and a natural order-theoretic structure is developed, demonstrated equivalent to Boolean algebras, and extended categorically to form a sound and complete semantics for this system. We show that all strong equivalences of reversible logic circuits are provable in the system, derive an equivalent equational theory, and describe its main applications in the verification of both reversible circuits and template-based reversible circuit rewriting systems.

TitelLogic, Language, Information, and Computation - 23rd International Workshop, WoLLIC 2016, Proceedings
RedaktørerJouko Väänänen, Åsa Hirvonen, Ruy de Queiroz
ISBN (Trykt)9783662529201
StatusUdgivet - 2016

Bibliografisk note

DBLP's bibliographic metadata records provided through http://dblp.org/search/publ/api are distributed under a Creative Commons CC0 1.0 Universal Public Domain Dedication. Although the bibliographic metadata records are provided consistent with CC0 1.0 Dedication, the content described by the metadata records is not. Content may be subject to copyright, rights of privacy, rights of publicity and other restrictions.


Dyk ned i forskningsemnerne om 'A Classical Propositional Logic for Reasoning About Reversible Logic Circuits'. Sammen danner de et unikt fingeraftryk.