A Classical Propositional Logic for Reasoning About Reversible Logic Circuits View Full Text


Ontology type: schema:Chapter     


Chapter Info

DATE

2016

AUTHORS

Holger Bock Axelsen , Robert Glück , Robin Kaarsgaard

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. More... »

PAGES

52-67

References to SciGraph publications

Book

TITLE

Logic, Language, Information, and Computation

ISBN

978-3-662-52920-1
978-3-662-52921-8

Author Affiliations

Identifiers

URI

http://scigraph.springernature.com/pub.10.1007/978-3-662-52921-8_4

DOI

http://dx.doi.org/10.1007/978-3-662-52921-8_4

DIMENSIONS

https://app.dimensions.ai/details/publication/pub.1024463862


Indexing Status Check whether this publication has been indexed by Scopus and Web Of Science using the SN Indexing Status Tool
Incoming Citations Browse incoming citations for this publication using opencitations.net

JSON-LD is the canonical representation for SciGraph data.

TIP: You can open this SciGraph record using an external JSON-LD service: JSON-LD Playground Google SDTT

[
  {
    "@context": "https://springernature.github.io/scigraph/jsonld/sgcontext.json", 
    "about": [
      {
        "id": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/0802", 
        "inDefinedTermSet": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/", 
        "name": "Computation Theory and Mathematics", 
        "type": "DefinedTerm"
      }, 
      {
        "id": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/08", 
        "inDefinedTermSet": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/", 
        "name": "Information and Computing Sciences", 
        "type": "DefinedTerm"
      }
    ], 
    "author": [
      {
        "affiliation": {
          "alternateName": "University of Copenhagen", 
          "id": "https://www.grid.ac/institutes/grid.5254.6", 
          "name": [
            "DIKU, Department of Computer Science, University of Copenhagen"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Axelsen", 
        "givenName": "Holger Bock", 
        "id": "sg:person.015546427711.73", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.015546427711.73"
        ], 
        "type": "Person"
      }, 
      {
        "affiliation": {
          "alternateName": "University of Copenhagen", 
          "id": "https://www.grid.ac/institutes/grid.5254.6", 
          "name": [
            "DIKU, Department of Computer Science, University of Copenhagen"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Gl\u00fcck", 
        "givenName": "Robert", 
        "id": "sg:person.010754010217.31", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.010754010217.31"
        ], 
        "type": "Person"
      }, 
      {
        "affiliation": {
          "alternateName": "University of Copenhagen", 
          "id": "https://www.grid.ac/institutes/grid.5254.6", 
          "name": [
            "DIKU, Department of Computer Science, University of Copenhagen"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Kaarsgaard", 
        "givenName": "Robin", 
        "id": "sg:person.010156717467.69", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.010156717467.69"
        ], 
        "type": "Person"
      }
    ], 
    "citation": [
      {
        "id": "sg:pub.10.1007/3-540-10003-2_104", 
        "sameAs": [
          "https://app.dimensions.ai/details/publication/pub.1006731052", 
          "https://doi.org/10.1007/3-540-10003-2_104"
        ], 
        "type": "CreativeWork"
      }, 
      {
        "id": "https://doi.org/10.1006/aima.1993.1055", 
        "sameAs": [
          "https://app.dimensions.ai/details/publication/pub.1015926974"
        ], 
        "type": "CreativeWork"
      }, 
      {
        "id": "https://doi.org/10.1016/0001-8708(91)90003-p", 
        "sameAs": [
          "https://app.dimensions.ai/details/publication/pub.1016879688"
        ], 
        "type": "CreativeWork"
      }, 
      {
        "id": "sg:pub.10.1007/978-3-642-38986-3_16", 
        "sameAs": [
          "https://app.dimensions.ai/details/publication/pub.1028131994", 
          "https://doi.org/10.1007/978-3-642-38986-3_16"
        ], 
        "type": "CreativeWork"
      }, 
      {
        "id": "https://doi.org/10.1016/j.jlap.2009.02.006", 
        "sameAs": [
          "https://app.dimensions.ai/details/publication/pub.1028603771"
        ], 
        "type": "CreativeWork"
      }, 
      {
        "id": "https://doi.org/10.1145/1863523.1863525", 
        "sameAs": [
          "https://app.dimensions.ai/details/publication/pub.1030545021"
        ], 
        "type": "CreativeWork"
      }, 
      {
        "id": "sg:pub.10.1038/nature10872", 
        "sameAs": [
          "https://app.dimensions.ai/details/publication/pub.1036208115", 
          "https://doi.org/10.1038/nature10872"
        ], 
        "type": "CreativeWork"
      }, 
      {
        "id": "sg:pub.10.1007/bf01886518", 
        "sameAs": [
          "https://app.dimensions.ai/details/publication/pub.1037696840", 
          "https://doi.org/10.1007/bf01886518"
        ], 
        "type": "CreativeWork"
      }, 
      {
        "id": "sg:pub.10.1007/bf01886518", 
        "sameAs": [
          "https://app.dimensions.ai/details/publication/pub.1037696840", 
          "https://doi.org/10.1007/bf01886518"
        ], 
        "type": "CreativeWork"
      }, 
      {
        "id": "https://app.dimensions.ai/details/publication/pub.1045547780", 
        "type": "CreativeWork"
      }, 
      {
        "id": "https://app.dimensions.ai/details/publication/pub.1045547780", 
        "type": "CreativeWork"
      }, 
      {
        "id": "https://app.dimensions.ai/details/publication/pub.1048361522", 
        "type": "CreativeWork"
      }, 
      {
        "id": "sg:pub.10.1007/978-90-481-9579-4", 
        "sameAs": [
          "https://app.dimensions.ai/details/publication/pub.1048361522", 
          "https://doi.org/10.1007/978-90-481-9579-4"
        ], 
        "type": "CreativeWork"
      }, 
      {
        "id": "sg:pub.10.1007/978-90-481-9579-4", 
        "sameAs": [
          "https://app.dimensions.ai/details/publication/pub.1048361522", 
          "https://doi.org/10.1007/978-90-481-9579-4"
        ], 
        "type": "CreativeWork"
      }, 
      {
        "id": "https://doi.org/10.1088/1751-8113/43/38/382002", 
        "sameAs": [
          "https://app.dimensions.ai/details/publication/pub.1051840463"
        ], 
        "type": "CreativeWork"
      }, 
      {
        "id": "https://doi.org/10.1145/2088456.1863525", 
        "sameAs": [
          "https://app.dimensions.ai/details/publication/pub.1063160328"
        ], 
        "type": "CreativeWork"
      }, 
      {
        "id": "https://doi.org/10.1147/rd.53.0183", 
        "sameAs": [
          "https://app.dimensions.ai/details/publication/pub.1063183065"
        ], 
        "type": "CreativeWork"
      }, 
      {
        "id": "https://doi.org/10.7567/jjap.51.06fe10", 
        "sameAs": [
          "https://app.dimensions.ai/details/publication/pub.1073835516"
        ], 
        "type": "CreativeWork"
      }, 
      {
        "id": "https://doi.org/10.1090/conm/092/1003210", 
        "sameAs": [
          "https://app.dimensions.ai/details/publication/pub.1089206437"
        ], 
        "type": "CreativeWork"
      }, 
      {
        "id": "https://doi.org/10.1109/aspdac.2010.5419684", 
        "sameAs": [
          "https://app.dimensions.ai/details/publication/pub.1093551395"
        ], 
        "type": "CreativeWork"
      }, 
      {
        "id": "https://doi.org/10.1017/cbo9780511525896", 
        "sameAs": [
          "https://app.dimensions.ai/details/publication/pub.1098679857"
        ], 
        "type": "CreativeWork"
      }
    ], 
    "datePublished": "2016", 
    "datePublishedReg": "2016-01-01", 
    "description": "We propose a syntactic representation of reversible logic circuits in their entirety, based on Feynman\u2019s control interpretation of Toffoli\u2019s 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.", 
    "editor": [
      {
        "familyName": "V\u00e4\u00e4n\u00e4nen", 
        "givenName": "Jouko", 
        "type": "Person"
      }, 
      {
        "familyName": "Hirvonen", 
        "givenName": "\u00c5sa", 
        "type": "Person"
      }, 
      {
        "familyName": "de Queiroz", 
        "givenName": "Ruy", 
        "type": "Person"
      }
    ], 
    "genre": "chapter", 
    "id": "sg:pub.10.1007/978-3-662-52921-8_4", 
    "inLanguage": [
      "en"
    ], 
    "isAccessibleForFree": false, 
    "isPartOf": {
      "isbn": [
        "978-3-662-52920-1", 
        "978-3-662-52921-8"
      ], 
      "name": "Logic, Language, Information, and Computation", 
      "type": "Book"
    }, 
    "name": "A Classical Propositional Logic for Reasoning About Reversible Logic Circuits", 
    "pagination": "52-67", 
    "productId": [
      {
        "name": "doi", 
        "type": "PropertyValue", 
        "value": [
          "10.1007/978-3-662-52921-8_4"
        ]
      }, 
      {
        "name": "readcube_id", 
        "type": "PropertyValue", 
        "value": [
          "748c2f9652add01324d2bf7ba71dc799cf5663c5a8cfec52f29621a1ebd4d11e"
        ]
      }, 
      {
        "name": "dimensions_id", 
        "type": "PropertyValue", 
        "value": [
          "pub.1024463862"
        ]
      }
    ], 
    "publisher": {
      "location": "Berlin, Heidelberg", 
      "name": "Springer Berlin Heidelberg", 
      "type": "Organisation"
    }, 
    "sameAs": [
      "https://doi.org/10.1007/978-3-662-52921-8_4", 
      "https://app.dimensions.ai/details/publication/pub.1024463862"
    ], 
    "sdDataset": "chapters", 
    "sdDatePublished": "2019-04-15T18:11", 
    "sdLicense": "https://scigraph.springernature.com/explorer/license/", 
    "sdPublisher": {
      "name": "Springer Nature - SN SciGraph project", 
      "type": "Organization"
    }, 
    "sdSource": "s3://com-uberresearch-data-dimensions-target-20181106-alternative/cleanup/v134/2549eaecd7973599484d7c17b260dba0a4ecb94b/merge/v9/a6c9fde33151104705d4d7ff012ea9563521a3ce/jats-lookup/v90/0000000001_0000000264/records_8681_00000258.jsonl", 
    "type": "Chapter", 
    "url": "http://link.springer.com/10.1007/978-3-662-52921-8_4"
  }
]
 

Download the RDF metadata as:  json-ld nt turtle xml License info

HOW TO GET THIS DATA PROGRAMMATICALLY:

JSON-LD is a popular format for linked data which is fully compatible with JSON.

curl -H 'Accept: application/ld+json' 'https://scigraph.springernature.com/pub.10.1007/978-3-662-52921-8_4'

N-Triples is a line-based linked data format ideal for batch operations.

curl -H 'Accept: application/n-triples' 'https://scigraph.springernature.com/pub.10.1007/978-3-662-52921-8_4'

Turtle is a human-readable linked data format.

curl -H 'Accept: text/turtle' 'https://scigraph.springernature.com/pub.10.1007/978-3-662-52921-8_4'

RDF/XML is a standard XML format for linked data.

curl -H 'Accept: application/rdf+xml' 'https://scigraph.springernature.com/pub.10.1007/978-3-662-52921-8_4'


 

This table displays all metadata directly associated to this object as RDF triples.

146 TRIPLES      23 PREDICATES      45 URIs      20 LITERALS      8 BLANK NODES

Subject Predicate Object
1 sg:pub.10.1007/978-3-662-52921-8_4 schema:about anzsrc-for:08
2 anzsrc-for:0802
3 schema:author N348040939fb847c29902081303786a85
4 schema:citation sg:pub.10.1007/3-540-10003-2_104
5 sg:pub.10.1007/978-3-642-38986-3_16
6 sg:pub.10.1007/978-90-481-9579-4
7 sg:pub.10.1007/bf01886518
8 sg:pub.10.1038/nature10872
9 https://app.dimensions.ai/details/publication/pub.1045547780
10 https://app.dimensions.ai/details/publication/pub.1048361522
11 https://doi.org/10.1006/aima.1993.1055
12 https://doi.org/10.1016/0001-8708(91)90003-p
13 https://doi.org/10.1016/j.jlap.2009.02.006
14 https://doi.org/10.1017/cbo9780511525896
15 https://doi.org/10.1088/1751-8113/43/38/382002
16 https://doi.org/10.1090/conm/092/1003210
17 https://doi.org/10.1109/aspdac.2010.5419684
18 https://doi.org/10.1145/1863523.1863525
19 https://doi.org/10.1145/2088456.1863525
20 https://doi.org/10.1147/rd.53.0183
21 https://doi.org/10.7567/jjap.51.06fe10
22 schema:datePublished 2016
23 schema:datePublishedReg 2016-01-01
24 schema:description 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.
25 schema:editor Nd9bc68c55ec94271bb017ebac78ca164
26 schema:genre chapter
27 schema:inLanguage en
28 schema:isAccessibleForFree false
29 schema:isPartOf N219a31a3fe6d40bf82b0b0968b5b725f
30 schema:name A Classical Propositional Logic for Reasoning About Reversible Logic Circuits
31 schema:pagination 52-67
32 schema:productId N0623e81898c84e17a9788c1dd692a76b
33 Ncc704a02194847adbb404edc1c21ff92
34 Ncdf36b388fb04ee7a1d3c7166fe033b1
35 schema:publisher N06f89a2290de40e18ff121a916d10192
36 schema:sameAs https://app.dimensions.ai/details/publication/pub.1024463862
37 https://doi.org/10.1007/978-3-662-52921-8_4
38 schema:sdDatePublished 2019-04-15T18:11
39 schema:sdLicense https://scigraph.springernature.com/explorer/license/
40 schema:sdPublisher Nfd01285717cb486da6203e1da6c68b02
41 schema:url http://link.springer.com/10.1007/978-3-662-52921-8_4
42 sgo:license sg:explorer/license/
43 sgo:sdDataset chapters
44 rdf:type schema:Chapter
45 N0623e81898c84e17a9788c1dd692a76b schema:name doi
46 schema:value 10.1007/978-3-662-52921-8_4
47 rdf:type schema:PropertyValue
48 N06f89a2290de40e18ff121a916d10192 schema:location Berlin, Heidelberg
49 schema:name Springer Berlin Heidelberg
50 rdf:type schema:Organisation
51 N219a31a3fe6d40bf82b0b0968b5b725f schema:isbn 978-3-662-52920-1
52 978-3-662-52921-8
53 schema:name Logic, Language, Information, and Computation
54 rdf:type schema:Book
55 N348040939fb847c29902081303786a85 rdf:first sg:person.015546427711.73
56 rdf:rest N952da79730504060bd59585c5ea71905
57 N93e51cfcf71d47d0a6e5986b323b0bf2 rdf:first Nbd9a4b45b4964bd8b1430054ce9980c5
58 rdf:rest rdf:nil
59 N952da79730504060bd59585c5ea71905 rdf:first sg:person.010754010217.31
60 rdf:rest Ne98326f28b4b4c0bb2e2601fa2e9a221
61 Nabc0401268f84f13aa1815a3b704fc2f rdf:first Ne756c30826154f16ac65cfe62ef8d648
62 rdf:rest N93e51cfcf71d47d0a6e5986b323b0bf2
63 Nbd9a4b45b4964bd8b1430054ce9980c5 schema:familyName de Queiroz
64 schema:givenName Ruy
65 rdf:type schema:Person
66 Ncc704a02194847adbb404edc1c21ff92 schema:name dimensions_id
67 schema:value pub.1024463862
68 rdf:type schema:PropertyValue
69 Ncdf36b388fb04ee7a1d3c7166fe033b1 schema:name readcube_id
70 schema:value 748c2f9652add01324d2bf7ba71dc799cf5663c5a8cfec52f29621a1ebd4d11e
71 rdf:type schema:PropertyValue
72 Nd79fbf4206b9461eaddd28bcaf5fa8de schema:familyName Väänänen
73 schema:givenName Jouko
74 rdf:type schema:Person
75 Nd9bc68c55ec94271bb017ebac78ca164 rdf:first Nd79fbf4206b9461eaddd28bcaf5fa8de
76 rdf:rest Nabc0401268f84f13aa1815a3b704fc2f
77 Ne756c30826154f16ac65cfe62ef8d648 schema:familyName Hirvonen
78 schema:givenName Åsa
79 rdf:type schema:Person
80 Ne98326f28b4b4c0bb2e2601fa2e9a221 rdf:first sg:person.010156717467.69
81 rdf:rest rdf:nil
82 Nfd01285717cb486da6203e1da6c68b02 schema:name Springer Nature - SN SciGraph project
83 rdf:type schema:Organization
84 anzsrc-for:08 schema:inDefinedTermSet anzsrc-for:
85 schema:name Information and Computing Sciences
86 rdf:type schema:DefinedTerm
87 anzsrc-for:0802 schema:inDefinedTermSet anzsrc-for:
88 schema:name Computation Theory and Mathematics
89 rdf:type schema:DefinedTerm
90 sg:person.010156717467.69 schema:affiliation https://www.grid.ac/institutes/grid.5254.6
91 schema:familyName Kaarsgaard
92 schema:givenName Robin
93 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.010156717467.69
94 rdf:type schema:Person
95 sg:person.010754010217.31 schema:affiliation https://www.grid.ac/institutes/grid.5254.6
96 schema:familyName Glück
97 schema:givenName Robert
98 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.010754010217.31
99 rdf:type schema:Person
100 sg:person.015546427711.73 schema:affiliation https://www.grid.ac/institutes/grid.5254.6
101 schema:familyName Axelsen
102 schema:givenName Holger Bock
103 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.015546427711.73
104 rdf:type schema:Person
105 sg:pub.10.1007/3-540-10003-2_104 schema:sameAs https://app.dimensions.ai/details/publication/pub.1006731052
106 https://doi.org/10.1007/3-540-10003-2_104
107 rdf:type schema:CreativeWork
108 sg:pub.10.1007/978-3-642-38986-3_16 schema:sameAs https://app.dimensions.ai/details/publication/pub.1028131994
109 https://doi.org/10.1007/978-3-642-38986-3_16
110 rdf:type schema:CreativeWork
111 sg:pub.10.1007/978-90-481-9579-4 schema:sameAs https://app.dimensions.ai/details/publication/pub.1048361522
112 https://doi.org/10.1007/978-90-481-9579-4
113 rdf:type schema:CreativeWork
114 sg:pub.10.1007/bf01886518 schema:sameAs https://app.dimensions.ai/details/publication/pub.1037696840
115 https://doi.org/10.1007/bf01886518
116 rdf:type schema:CreativeWork
117 sg:pub.10.1038/nature10872 schema:sameAs https://app.dimensions.ai/details/publication/pub.1036208115
118 https://doi.org/10.1038/nature10872
119 rdf:type schema:CreativeWork
120 https://app.dimensions.ai/details/publication/pub.1045547780 schema:CreativeWork
121 https://app.dimensions.ai/details/publication/pub.1048361522 schema:CreativeWork
122 https://doi.org/10.1006/aima.1993.1055 schema:sameAs https://app.dimensions.ai/details/publication/pub.1015926974
123 rdf:type schema:CreativeWork
124 https://doi.org/10.1016/0001-8708(91)90003-p schema:sameAs https://app.dimensions.ai/details/publication/pub.1016879688
125 rdf:type schema:CreativeWork
126 https://doi.org/10.1016/j.jlap.2009.02.006 schema:sameAs https://app.dimensions.ai/details/publication/pub.1028603771
127 rdf:type schema:CreativeWork
128 https://doi.org/10.1017/cbo9780511525896 schema:sameAs https://app.dimensions.ai/details/publication/pub.1098679857
129 rdf:type schema:CreativeWork
130 https://doi.org/10.1088/1751-8113/43/38/382002 schema:sameAs https://app.dimensions.ai/details/publication/pub.1051840463
131 rdf:type schema:CreativeWork
132 https://doi.org/10.1090/conm/092/1003210 schema:sameAs https://app.dimensions.ai/details/publication/pub.1089206437
133 rdf:type schema:CreativeWork
134 https://doi.org/10.1109/aspdac.2010.5419684 schema:sameAs https://app.dimensions.ai/details/publication/pub.1093551395
135 rdf:type schema:CreativeWork
136 https://doi.org/10.1145/1863523.1863525 schema:sameAs https://app.dimensions.ai/details/publication/pub.1030545021
137 rdf:type schema:CreativeWork
138 https://doi.org/10.1145/2088456.1863525 schema:sameAs https://app.dimensions.ai/details/publication/pub.1063160328
139 rdf:type schema:CreativeWork
140 https://doi.org/10.1147/rd.53.0183 schema:sameAs https://app.dimensions.ai/details/publication/pub.1063183065
141 rdf:type schema:CreativeWork
142 https://doi.org/10.7567/jjap.51.06fe10 schema:sameAs https://app.dimensions.ai/details/publication/pub.1073835516
143 rdf:type schema:CreativeWork
144 https://www.grid.ac/institutes/grid.5254.6 schema:alternateName University of Copenhagen
145 schema:name DIKU, Department of Computer Science, University of Copenhagen
146 rdf:type schema:Organization
 




Preview window. Press ESC to close (or click here)


...