A Classical Propositional Logic for Reasoning About Reversible Logic Circuits

Holger Bock Axelsen, Robert Glück, Robin Kaarsgaard

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

Abstract

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.

Original languageEnglish
Title of host publicationLogic, Language, Information, and Computation - 23rd International Workshop, WoLLIC 2016, Proceedings
EditorsJouko Väänänen, Åsa Hirvonen, Ruy de Queiroz
Publication date2016
Pages52-67
ISBN (Print)9783662529201
DOIs
Publication statusPublished - 2016

Bibliographical 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.

Fingerprint

Dive into the research topics of 'A Classical Propositional Logic for Reasoning About Reversible Logic Circuits'. Together they form a unique fingerprint.

Cite this