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

Datalogisk Institut

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.

Originalsprog	Engelsk
Titel	Logic, Language, Information, and Computation : 23rd International Workshop, WoLLIC 2016, Puebla, Mexico, August 16-19th, 2016. Proceedings
Redaktører	Jouko Väänänen, Åsa Hirvonen, Ruy de Queiroz
Antal sider	16
Forlag	Springer
Publikationsdato	2016
Sider	52-67
ISBN (Trykt)	978-3-662-52920-1
ISBN (Elektronisk)	978-3-662-52921-8
DOI	https://doi.org/10.1007/978-3-662-52921-8_4
Status	Udgivet - 2016
Begivenhed	23rd International Workshop on Logic, Language, Information and Computation - Puebla, Mexico Varighed: 16 aug. 2016 → 19 aug. 2016 Konferencens nummer: 23

Konference

Konference	23rd International Workshop on Logic, Language, Information and Computation
Nummer	23
Land/Område	Mexico
By	Puebla
Periode	16/08/2016 → 19/08/2016

Navn	Lecture notes in computer science
Vol/bind	9803
ISSN	0302-9743

Adgang til dokumentet

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

Citationsformater

Axelsen, H. B., Glück, R., & Kaarsgaard, R. (2016). A classical propositional logic for reasoning about reversible logic circuits. I J. Väänänen, Å. Hirvonen, & R. de Queiroz (red.), Logic, Language, Information, and Computation: 23rd International Workshop, WoLLIC 2016, Puebla, Mexico, August 16-19th, 2016. Proceedings (s. 52-67). Springer. 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. red. / Jouko Väänänen; Åsa Hirvonen; Ruy de Queiroz. Springer, 2016. s. 52-67 (Lecture notes in computer science, Bind 9803).

Publikation: Bidrag til bog/antologi/rapport › Konferencebidrag i proceedings › Forskning › peer review

Axelsen, HB, Glück, R & Kaarsgaard, R 2016, A classical propositional logic for reasoning about reversible logic circuits. i J Väänänen, Å Hirvonen & R de Queiroz (red), Logic, Language, Information, and Computation: 23rd International Workshop, WoLLIC 2016, Puebla, Mexico, August 16-19th, 2016. Proceedings. Springer, Lecture notes in computer science, bind 9803, s. 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. I Väänänen J, Hirvonen Å, de Queiroz R, red., Logic, Language, Information, and Computation: 23rd International Workshop, WoLLIC 2016, Puebla, Mexico, August 16-19th, 2016. Proceedings. Springer. 2016. s. 52-67. (Lecture notes in computer science, Bind 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. red. / Jouko Väänänen ; Åsa Hirvonen ; Ruy de Queiroz. Springer, 2016. s. 52-67 (Lecture notes in computer science, Bind 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

Konference

Adgang til dokumentet

Fingeraftryk

Citationsformater