Strict Canonical Constructive Systems View Full Text


Ontology type: schema:Chapter      Open Access: True


Chapter Info

DATE

2010

AUTHORS

Arnon Avron , Ori Lahav

ABSTRACT

We define the notions of a canonical inference rule and a canonical constructive system in the framework of strict single-conclusion Gentzen-type systems (or, equivalently, natural deduction systems), and develop a corresponding general non-deterministic Kripke-style semantics. We show that every strict constructive canonical system induces a class of non-deterministic Kripke-style frames, for which it is strongly sound and complete. This non-deterministic semantics is used for proving a strong form of the cut-elimination theorem for such systems, and for providing a decision procedure for them. These results identify a large family of basic constructive connectives, including the standard intuitionistic connectives, together with many other independent connectives. More... »

PAGES

75-94

References to SciGraph publications

  • 2009. Canonical Constructive Systems in AUTOMATED REASONING WITH ANALYTIC TABLEAUX AND RELATED METHODS
  • 2005-08. A Non-deterministic View on Non-classical Negations in STUDIA LOGICA
  • 2006-02. Towards a Semantic Characterization of Cut-Elimination in STUDIA LOGICA
  • 1993-06. Gentzen-type systems, resolution and tableaux in JOURNAL OF AUTOMATED REASONING
  • 2001-06-08. Canonical Propositional Gentzen-Type Systems in AUTOMATED REASONING
  • 2002. Proof Theory and Meaning in HANDBOOK OF PHILOSOPHICAL LOGIC
  • Book

    TITLE

    Fields of Logic and Computation

    ISBN

    978-3-642-15024-1
    978-3-642-15025-8

    Author Affiliations

    Identifiers

    URI

    http://scigraph.springernature.com/pub.10.1007/978-3-642-15025-8_4

    DOI

    http://dx.doi.org/10.1007/978-3-642-15025-8_4

    DIMENSIONS

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


    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/0801", 
            "inDefinedTermSet": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/", 
            "name": "Artificial Intelligence and Image Processing", 
            "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": "Tel Aviv University", 
              "id": "https://www.grid.ac/institutes/grid.12136.37", 
              "name": [
                "School of Computer Science, Tel Aviv University, Israel"
              ], 
              "type": "Organization"
            }, 
            "familyName": "Avron", 
            "givenName": "Arnon", 
            "id": "sg:person.014461136355.70", 
            "sameAs": [
              "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.014461136355.70"
            ], 
            "type": "Person"
          }, 
          {
            "affiliation": {
              "alternateName": "Tel Aviv University", 
              "id": "https://www.grid.ac/institutes/grid.12136.37", 
              "name": [
                "School of Computer Science, Tel Aviv University, Israel"
              ], 
              "type": "Organization"
            }, 
            "familyName": "Lahav", 
            "givenName": "Ori", 
            "id": "sg:person.011457433253.13", 
            "sameAs": [
              "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.011457433253.13"
            ], 
            "type": "Person"
          }
        ], 
        "citation": [
          {
            "id": "https://doi.org/10.1016/s0049-237x(08)71685-9", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1003546056"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/bf00881838", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1007496843", 
              "https://doi.org/10.1007/bf00881838"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/s11225-006-6607-2", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1007969950", 
              "https://doi.org/10.1007/s11225-006-6607-2"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/s11225-006-6607-2", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1007969950", 
              "https://doi.org/10.1007/s11225-006-6607-2"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1016/j.apal.2008.09.015", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1008628061"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/978-94-017-0464-9_3", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1011250122", 
              "https://doi.org/10.1007/978-94-017-0464-9_3"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1145/1877714.1877715", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1039018409"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1016/0890-5401(91)90023-u", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1041008858"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/978-3-642-02716-1_6", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1043408055", 
              "https://doi.org/10.1007/978-3-642-02716-1_6"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/978-3-642-02716-1_6", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1043408055", 
              "https://doi.org/10.1007/978-3-642-02716-1_6"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/s11225-005-8468-5", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1051156700", 
              "https://doi.org/10.1007/s11225-005-8468-5"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/s11225-005-8468-5", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1051156700", 
              "https://doi.org/10.1007/s11225-005-8468-5"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/s11225-005-8468-5", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1051156700", 
              "https://doi.org/10.1007/s11225-005-8468-5"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/3-540-45744-5_45", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1051434466", 
              "https://doi.org/10.1007/3-540-45744-5_45"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/3-540-45744-5_45", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1051434466", 
              "https://doi.org/10.1007/3-540-45744-5_45"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1093/analys/21.2.38", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1059386429"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1093/analys/22.6.130", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1059386488"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1093/logcom/exi001", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1059875940"
            ], 
            "type": "CreativeWork"
          }
        ], 
        "datePublished": "2010", 
        "datePublishedReg": "2010-01-01", 
        "description": "We define the notions of a canonical inference rule and a canonical constructive system in the framework of strict single-conclusion Gentzen-type systems (or, equivalently, natural deduction systems), and develop a corresponding general non-deterministic Kripke-style semantics. We show that every strict constructive canonical system induces a class of non-deterministic Kripke-style frames, for which it is strongly sound and complete. This non-deterministic semantics is used for proving a strong form of the cut-elimination theorem for such systems, and for providing a decision procedure for them. These results identify a large family of basic constructive connectives, including the standard intuitionistic connectives, together with many other independent connectives.", 
        "editor": [
          {
            "familyName": "Blass", 
            "givenName": "Andreas", 
            "type": "Person"
          }, 
          {
            "familyName": "Dershowitz", 
            "givenName": "Nachum", 
            "type": "Person"
          }, 
          {
            "familyName": "Reisig", 
            "givenName": "Wolfgang", 
            "type": "Person"
          }
        ], 
        "genre": "chapter", 
        "id": "sg:pub.10.1007/978-3-642-15025-8_4", 
        "inLanguage": [
          "en"
        ], 
        "isAccessibleForFree": true, 
        "isPartOf": {
          "isbn": [
            "978-3-642-15024-1", 
            "978-3-642-15025-8"
          ], 
          "name": "Fields of Logic and Computation", 
          "type": "Book"
        }, 
        "name": "Strict Canonical Constructive Systems", 
        "pagination": "75-94", 
        "productId": [
          {
            "name": "doi", 
            "type": "PropertyValue", 
            "value": [
              "10.1007/978-3-642-15025-8_4"
            ]
          }, 
          {
            "name": "readcube_id", 
            "type": "PropertyValue", 
            "value": [
              "9e7d5008becb7f6b47e84efef3f234b2aae56b1eadfa92204c79c72e0efe3ab1"
            ]
          }, 
          {
            "name": "dimensions_id", 
            "type": "PropertyValue", 
            "value": [
              "pub.1033269122"
            ]
          }
        ], 
        "publisher": {
          "location": "Berlin, Heidelberg", 
          "name": "Springer Berlin Heidelberg", 
          "type": "Organisation"
        }, 
        "sameAs": [
          "https://doi.org/10.1007/978-3-642-15025-8_4", 
          "https://app.dimensions.ai/details/publication/pub.1033269122"
        ], 
        "sdDataset": "chapters", 
        "sdDatePublished": "2019-04-15T17:45", 
        "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_8678_00000546.jsonl", 
        "type": "Chapter", 
        "url": "http://link.springer.com/10.1007/978-3-642-15025-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-642-15025-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-642-15025-8_4'

    Turtle is a human-readable linked data format.

    curl -H 'Accept: text/turtle' 'https://scigraph.springernature.com/pub.10.1007/978-3-642-15025-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-642-15025-8_4'


     

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

    127 TRIPLES      23 PREDICATES      40 URIs      20 LITERALS      8 BLANK NODES

    Subject Predicate Object
    1 sg:pub.10.1007/978-3-642-15025-8_4 schema:about anzsrc-for:08
    2 anzsrc-for:0801
    3 schema:author N372fd619ea7546809b74094fca669941
    4 schema:citation sg:pub.10.1007/3-540-45744-5_45
    5 sg:pub.10.1007/978-3-642-02716-1_6
    6 sg:pub.10.1007/978-94-017-0464-9_3
    7 sg:pub.10.1007/bf00881838
    8 sg:pub.10.1007/s11225-005-8468-5
    9 sg:pub.10.1007/s11225-006-6607-2
    10 https://doi.org/10.1016/0890-5401(91)90023-u
    11 https://doi.org/10.1016/j.apal.2008.09.015
    12 https://doi.org/10.1016/s0049-237x(08)71685-9
    13 https://doi.org/10.1093/analys/21.2.38
    14 https://doi.org/10.1093/analys/22.6.130
    15 https://doi.org/10.1093/logcom/exi001
    16 https://doi.org/10.1145/1877714.1877715
    17 schema:datePublished 2010
    18 schema:datePublishedReg 2010-01-01
    19 schema:description We define the notions of a canonical inference rule and a canonical constructive system in the framework of strict single-conclusion Gentzen-type systems (or, equivalently, natural deduction systems), and develop a corresponding general non-deterministic Kripke-style semantics. We show that every strict constructive canonical system induces a class of non-deterministic Kripke-style frames, for which it is strongly sound and complete. This non-deterministic semantics is used for proving a strong form of the cut-elimination theorem for such systems, and for providing a decision procedure for them. These results identify a large family of basic constructive connectives, including the standard intuitionistic connectives, together with many other independent connectives.
    20 schema:editor Nbfd7bd2c94484dbc8a27094ead7cce80
    21 schema:genre chapter
    22 schema:inLanguage en
    23 schema:isAccessibleForFree true
    24 schema:isPartOf N0af0e8eb7fa6494697d3f3244bfae865
    25 schema:name Strict Canonical Constructive Systems
    26 schema:pagination 75-94
    27 schema:productId N4490dc2d52cf4011ac1006e1f67af28c
    28 N9df6a761bf324b8bbea96937dfe4fee5
    29 Nab49f26e3dfd4c08aec7a09094d02ee5
    30 schema:publisher N35d30bf7b1ad445fa6a224e14d4f94c4
    31 schema:sameAs https://app.dimensions.ai/details/publication/pub.1033269122
    32 https://doi.org/10.1007/978-3-642-15025-8_4
    33 schema:sdDatePublished 2019-04-15T17:45
    34 schema:sdLicense https://scigraph.springernature.com/explorer/license/
    35 schema:sdPublisher N74324e0c157d4c428bf35dd459425096
    36 schema:url http://link.springer.com/10.1007/978-3-642-15025-8_4
    37 sgo:license sg:explorer/license/
    38 sgo:sdDataset chapters
    39 rdf:type schema:Chapter
    40 N0af0e8eb7fa6494697d3f3244bfae865 schema:isbn 978-3-642-15024-1
    41 978-3-642-15025-8
    42 schema:name Fields of Logic and Computation
    43 rdf:type schema:Book
    44 N35d30bf7b1ad445fa6a224e14d4f94c4 schema:location Berlin, Heidelberg
    45 schema:name Springer Berlin Heidelberg
    46 rdf:type schema:Organisation
    47 N372fd619ea7546809b74094fca669941 rdf:first sg:person.014461136355.70
    48 rdf:rest N45615d61381541adb1e9e5b04ba04add
    49 N4490dc2d52cf4011ac1006e1f67af28c schema:name dimensions_id
    50 schema:value pub.1033269122
    51 rdf:type schema:PropertyValue
    52 N45615d61381541adb1e9e5b04ba04add rdf:first sg:person.011457433253.13
    53 rdf:rest rdf:nil
    54 N5f6c914527ed4e54942b65daddb017d9 rdf:first N60fff701974146cb91b2c91f4e18d0e6
    55 rdf:rest rdf:nil
    56 N60fff701974146cb91b2c91f4e18d0e6 schema:familyName Reisig
    57 schema:givenName Wolfgang
    58 rdf:type schema:Person
    59 N6813ce1e648a492ca0ddca926b8b6e03 rdf:first Nb7f45e1c049d490b97c6ad0ede525aa4
    60 rdf:rest N5f6c914527ed4e54942b65daddb017d9
    61 N74324e0c157d4c428bf35dd459425096 schema:name Springer Nature - SN SciGraph project
    62 rdf:type schema:Organization
    63 N9df6a761bf324b8bbea96937dfe4fee5 schema:name readcube_id
    64 schema:value 9e7d5008becb7f6b47e84efef3f234b2aae56b1eadfa92204c79c72e0efe3ab1
    65 rdf:type schema:PropertyValue
    66 Nab49f26e3dfd4c08aec7a09094d02ee5 schema:name doi
    67 schema:value 10.1007/978-3-642-15025-8_4
    68 rdf:type schema:PropertyValue
    69 Nb7f45e1c049d490b97c6ad0ede525aa4 schema:familyName Dershowitz
    70 schema:givenName Nachum
    71 rdf:type schema:Person
    72 Nbfd7bd2c94484dbc8a27094ead7cce80 rdf:first Nc445bba3226f439dab816da76ef5d7c9
    73 rdf:rest N6813ce1e648a492ca0ddca926b8b6e03
    74 Nc445bba3226f439dab816da76ef5d7c9 schema:familyName Blass
    75 schema:givenName Andreas
    76 rdf:type schema:Person
    77 anzsrc-for:08 schema:inDefinedTermSet anzsrc-for:
    78 schema:name Information and Computing Sciences
    79 rdf:type schema:DefinedTerm
    80 anzsrc-for:0801 schema:inDefinedTermSet anzsrc-for:
    81 schema:name Artificial Intelligence and Image Processing
    82 rdf:type schema:DefinedTerm
    83 sg:person.011457433253.13 schema:affiliation https://www.grid.ac/institutes/grid.12136.37
    84 schema:familyName Lahav
    85 schema:givenName Ori
    86 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.011457433253.13
    87 rdf:type schema:Person
    88 sg:person.014461136355.70 schema:affiliation https://www.grid.ac/institutes/grid.12136.37
    89 schema:familyName Avron
    90 schema:givenName Arnon
    91 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.014461136355.70
    92 rdf:type schema:Person
    93 sg:pub.10.1007/3-540-45744-5_45 schema:sameAs https://app.dimensions.ai/details/publication/pub.1051434466
    94 https://doi.org/10.1007/3-540-45744-5_45
    95 rdf:type schema:CreativeWork
    96 sg:pub.10.1007/978-3-642-02716-1_6 schema:sameAs https://app.dimensions.ai/details/publication/pub.1043408055
    97 https://doi.org/10.1007/978-3-642-02716-1_6
    98 rdf:type schema:CreativeWork
    99 sg:pub.10.1007/978-94-017-0464-9_3 schema:sameAs https://app.dimensions.ai/details/publication/pub.1011250122
    100 https://doi.org/10.1007/978-94-017-0464-9_3
    101 rdf:type schema:CreativeWork
    102 sg:pub.10.1007/bf00881838 schema:sameAs https://app.dimensions.ai/details/publication/pub.1007496843
    103 https://doi.org/10.1007/bf00881838
    104 rdf:type schema:CreativeWork
    105 sg:pub.10.1007/s11225-005-8468-5 schema:sameAs https://app.dimensions.ai/details/publication/pub.1051156700
    106 https://doi.org/10.1007/s11225-005-8468-5
    107 rdf:type schema:CreativeWork
    108 sg:pub.10.1007/s11225-006-6607-2 schema:sameAs https://app.dimensions.ai/details/publication/pub.1007969950
    109 https://doi.org/10.1007/s11225-006-6607-2
    110 rdf:type schema:CreativeWork
    111 https://doi.org/10.1016/0890-5401(91)90023-u schema:sameAs https://app.dimensions.ai/details/publication/pub.1041008858
    112 rdf:type schema:CreativeWork
    113 https://doi.org/10.1016/j.apal.2008.09.015 schema:sameAs https://app.dimensions.ai/details/publication/pub.1008628061
    114 rdf:type schema:CreativeWork
    115 https://doi.org/10.1016/s0049-237x(08)71685-9 schema:sameAs https://app.dimensions.ai/details/publication/pub.1003546056
    116 rdf:type schema:CreativeWork
    117 https://doi.org/10.1093/analys/21.2.38 schema:sameAs https://app.dimensions.ai/details/publication/pub.1059386429
    118 rdf:type schema:CreativeWork
    119 https://doi.org/10.1093/analys/22.6.130 schema:sameAs https://app.dimensions.ai/details/publication/pub.1059386488
    120 rdf:type schema:CreativeWork
    121 https://doi.org/10.1093/logcom/exi001 schema:sameAs https://app.dimensions.ai/details/publication/pub.1059875940
    122 rdf:type schema:CreativeWork
    123 https://doi.org/10.1145/1877714.1877715 schema:sameAs https://app.dimensions.ai/details/publication/pub.1039018409
    124 rdf:type schema:CreativeWork
    125 https://www.grid.ac/institutes/grid.12136.37 schema:alternateName Tel Aviv University
    126 schema:name School of Computer Science, Tel Aviv University, Israel
    127 rdf:type schema:Organization
     




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


    ...