A classical propositional logic for reasoning about reversible logic circuits

Holger Bock Axelsen; Robert Glück; Robin Kaarsgaard

doi:10.1007/978-3-662-52921-8_4

A classical propositional logic for reasoning about reversible logic circuits

Holger Bock Axelsen, Robert Glück, Robin Kaarsgaard

Department of Computer Science

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 language	English
Title of host publication	Logic, Language, Information, and Computation : 23rd International Workshop, WoLLIC 2016, Puebla, Mexico, August 16-19th, 2016. Proceedings
Editors	Jouko Väänänen, Åsa Hirvonen, Ruy de Queiroz
Number of pages	16
Publisher	Springer
Publication date	2016
Pages	52-67
ISBN (Print)	978-3-662-52920-1
ISBN (Electronic)	978-3-662-52921-8
DOIs	https://doi.org/10.1007/978-3-662-52921-8_4
Publication status	Published - 2016
Event	23rd International Workshop on Logic, Language, Information and Computation - Puebla, Mexico Duration: 16 Aug 2016 → 19 Aug 2016 Conference number: 23

Conference

Conference	23rd International Workshop on Logic, Language, Information and Computation
Number	23
Country/Territory	Mexico
City	Puebla
Period	16/08/2016 → 19/08/2016

Series	Lecture notes in computer science
Volume	9803
ISSN	0302-9743

Access to Document

10.1007/978-3-662-52921-8_4

Cite this

Axelsen, H. B., Glück, R., & Kaarsgaard, R. (2016). A classical propositional logic for reasoning about reversible logic circuits. In J. Väänänen, Å. Hirvonen, & R. de Queiroz (Eds.), Logic, Language, Information, and Computation: 23rd International Workshop, WoLLIC 2016, Puebla, Mexico, August 16-19th, 2016. Proceedings (pp. 52-67). Springer. Lecture notes in computer science Vol. 9803 https://doi.org/10.1007/978-3-662-52921-8_4

A classical propositional logic for reasoning about reversible logic circuits. / Axelsen, Holger Bock; Glück, Robert ; Kaarsgaard, Robin.

Logic, Language, Information, and Computation: 23rd International Workshop, WoLLIC 2016, Puebla, Mexico, August 16-19th, 2016. Proceedings. ed. / Jouko Väänänen; Åsa Hirvonen; Ruy de Queiroz. Springer, 2016. p. 52-67 (Lecture notes in computer science, Vol. 9803).

Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review

Axelsen, HB, Glück, R & Kaarsgaard, R 2016, A classical propositional logic for reasoning about reversible logic circuits. in J Väänänen, Å Hirvonen & R de Queiroz (eds), Logic, Language, Information, and Computation: 23rd International Workshop, WoLLIC 2016, Puebla, Mexico, August 16-19th, 2016. Proceedings. Springer, Lecture notes in computer science, vol. 9803, pp. 52-67, 23rd International Workshop on Logic, Language, Information and Computation, Puebla, Mexico, 16/08/2016. https://doi.org/10.1007/978-3-662-52921-8_4

Axelsen HB, Glück R , Kaarsgaard R. A classical propositional logic for reasoning about reversible logic circuits. In Väänänen J, Hirvonen Å, de Queiroz R, editors, Logic, Language, Information, and Computation: 23rd International Workshop, WoLLIC 2016, Puebla, Mexico, August 16-19th, 2016. Proceedings. Springer. 2016. p. 52-67. (Lecture notes in computer science, Vol. 9803). doi: 10.1007/978-3-662-52921-8_4

Axelsen, Holger Bock ; Glück, Robert ; Kaarsgaard, Robin. / A classical propositional logic for reasoning about reversible logic circuits. Logic, Language, Information, and Computation: 23rd International Workshop, WoLLIC 2016, Puebla, Mexico, August 16-19th, 2016. Proceedings. editor / Jouko Väänänen ; Åsa Hirvonen ; Ruy de Queiroz. Springer, 2016. pp. 52-67 (Lecture notes in computer science, Vol. 9803).

@inproceedings{f9c75887f1b3497e9174e83547aca620,

title = "A classical propositional logic for reasoning about reversible logic circuits",

abstract = "We propose a syntactic representation of reversible logic circuits in their entirety, based on Feynman{\textquoteright}s control interpretation of Toffoli{\textquoteright}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.",

author = "Axelsen, {Holger Bock} and Robert Gl{\"u}ck and Robin Kaarsgaard",

year = "2016",

doi = "10.1007/978-3-662-52921-8_4",

language = "English",

isbn = "978-3-662-52920-1",

series = "Lecture notes in computer science",

publisher = "Springer",

pages = "52--67",

editor = "Jouko V{\"a}{\"a}n{\"a}nen and {\AA}sa Hirvonen and {de Queiroz}, Ruy",

booktitle = "Logic, Language, Information, and Computation",

note = "23rd International Workshop on Logic, Language, Information and Computation ; Conference date: 16-08-2016 Through 19-08-2016",

}

TY - GEN

T1 - A classical propositional logic for reasoning about reversible logic circuits

AU - Axelsen, Holger Bock

AU - Glück, Robert

AU - Kaarsgaard, Robin

N1 - Conference code: 23

PY - 2016

Y1 - 2016

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

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

U2 - 10.1007/978-3-662-52921-8_4

DO - 10.1007/978-3-662-52921-8_4

M3 - Article in proceedings

SN - 978-3-662-52920-1

T3 - Lecture notes in computer science

SP - 52

EP - 67

BT - Logic, Language, Information, and Computation

A2 - Väänänen, Jouko

A2 - Hirvonen, Åsa

A2 - de Queiroz, Ruy

PB - Springer

T2 - 23rd International Workshop on Logic, Language, Information and Computation

Y2 - 16 August 2016 through 19 August 2016

ER -

A classical propositional logic for reasoning about reversible logic circuits

Abstract

Conference

Access to Document

Fingerprint

Cite this