Canonical Constructive Systems View Full Text


Ontology type: schema:Chapter      Open Access: True


Chapter Info

DATE

2009

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 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 to show that such a system always admits a strong form of the cut-elimination theorem, and for providing a decision procedure for such systems. More... »

PAGES

62-76

References to SciGraph publications

  • 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
  • 2005-08. A Non-deterministic View on Non-classical Negations in STUDIA LOGICA
  • 2002. Proof Theory and Meaning in HANDBOOK OF PHILOSOPHICAL LOGIC
  • Book

    TITLE

    Automated Reasoning with Analytic Tableaux and Related Methods

    ISBN

    978-3-642-02715-4
    978-3-642-02716-1

    Author Affiliations

    Identifiers

    URI

    http://scigraph.springernature.com/pub.10.1007/978-3-642-02716-1_6

    DOI

    http://dx.doi.org/10.1007/978-3-642-02716-1_6

    DIMENSIONS

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


    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.1016/0890-5401(91)90023-u", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1041008858"
            ], 
            "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/logcom/exi001", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1059875940"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.2307/2271192", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1069855852"
            ], 
            "type": "CreativeWork"
          }
        ], 
        "datePublished": "2009", 
        "datePublishedReg": "2009-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 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 to show that such a system always admits a strong form of the cut-elimination theorem, and for providing a decision procedure for such systems.", 
        "editor": [
          {
            "familyName": "Giese", 
            "givenName": "Martin", 
            "type": "Person"
          }, 
          {
            "familyName": "Waaler", 
            "givenName": "Arild", 
            "type": "Person"
          }
        ], 
        "genre": "chapter", 
        "id": "sg:pub.10.1007/978-3-642-02716-1_6", 
        "inLanguage": [
          "en"
        ], 
        "isAccessibleForFree": true, 
        "isPartOf": {
          "isbn": [
            "978-3-642-02715-4", 
            "978-3-642-02716-1"
          ], 
          "name": "Automated Reasoning with Analytic Tableaux and Related Methods", 
          "type": "Book"
        }, 
        "name": "Canonical Constructive Systems", 
        "pagination": "62-76", 
        "productId": [
          {
            "name": "dimensions_id", 
            "type": "PropertyValue", 
            "value": [
              "pub.1043408055"
            ]
          }, 
          {
            "name": "doi", 
            "type": "PropertyValue", 
            "value": [
              "10.1007/978-3-642-02716-1_6"
            ]
          }, 
          {
            "name": "readcube_id", 
            "type": "PropertyValue", 
            "value": [
              "cec4c0dbb0759e2faf7c1ec5a0f96f738021a94004b808430caf40f127e4029b"
            ]
          }
        ], 
        "publisher": {
          "location": "Berlin, Heidelberg", 
          "name": "Springer Berlin Heidelberg", 
          "type": "Organisation"
        }, 
        "sameAs": [
          "https://doi.org/10.1007/978-3-642-02716-1_6", 
          "https://app.dimensions.ai/details/publication/pub.1043408055"
        ], 
        "sdDataset": "chapters", 
        "sdDatePublished": "2019-04-16T07:27", 
        "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/0000000355_0000000355/records_53014_00000000.jsonl", 
        "type": "Chapter", 
        "url": "https://link.springer.com/10.1007%2F978-3-642-02716-1_6"
      }
    ]
     

    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-02716-1_6'

    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-02716-1_6'

    Turtle is a human-readable linked data format.

    curl -H 'Accept: text/turtle' 'https://scigraph.springernature.com/pub.10.1007/978-3-642-02716-1_6'

    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-02716-1_6'


     

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

    112 TRIPLES      23 PREDICATES      37 URIs      20 LITERALS      8 BLANK NODES

    Subject Predicate Object
    1 sg:pub.10.1007/978-3-642-02716-1_6 schema:about anzsrc-for:08
    2 anzsrc-for:0801
    3 schema:author N7262e2bf59ae495d9d561604244a61cd
    4 schema:citation sg:pub.10.1007/3-540-45744-5_45
    5 sg:pub.10.1007/978-94-017-0464-9_3
    6 sg:pub.10.1007/bf00881838
    7 sg:pub.10.1007/s11225-005-8468-5
    8 sg:pub.10.1007/s11225-006-6607-2
    9 https://doi.org/10.1016/0890-5401(91)90023-u
    10 https://doi.org/10.1016/j.apal.2008.09.015
    11 https://doi.org/10.1016/s0049-237x(08)71685-9
    12 https://doi.org/10.1093/logcom/exi001
    13 https://doi.org/10.2307/2271192
    14 schema:datePublished 2009
    15 schema:datePublishedReg 2009-01-01
    16 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 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 to show that such a system always admits a strong form of the cut-elimination theorem, and for providing a decision procedure for such systems.
    17 schema:editor N0220b27526464dabb9ba71d0a80f2d0d
    18 schema:genre chapter
    19 schema:inLanguage en
    20 schema:isAccessibleForFree true
    21 schema:isPartOf Na30c78f6d29a41f89403a43e2155019c
    22 schema:name Canonical Constructive Systems
    23 schema:pagination 62-76
    24 schema:productId N4936c09b88e641dd8dfc431fca9d0a6e
    25 Na000cf58ea8e410d95cbe1c6fd6d9da4
    26 Ne6265c06e6b04c81870a53b8f905b05d
    27 schema:publisher N3f476947239f49e3b2b3f5753378b70b
    28 schema:sameAs https://app.dimensions.ai/details/publication/pub.1043408055
    29 https://doi.org/10.1007/978-3-642-02716-1_6
    30 schema:sdDatePublished 2019-04-16T07:27
    31 schema:sdLicense https://scigraph.springernature.com/explorer/license/
    32 schema:sdPublisher Ne243188291524cb691a75f1f3a5c8f04
    33 schema:url https://link.springer.com/10.1007%2F978-3-642-02716-1_6
    34 sgo:license sg:explorer/license/
    35 sgo:sdDataset chapters
    36 rdf:type schema:Chapter
    37 N0220b27526464dabb9ba71d0a80f2d0d rdf:first N33c9174805084be2ac463ce56c089f1d
    38 rdf:rest Ne1131fa8bcdf4459ae4861f1dff55a8d
    39 N33c9174805084be2ac463ce56c089f1d schema:familyName Giese
    40 schema:givenName Martin
    41 rdf:type schema:Person
    42 N3f476947239f49e3b2b3f5753378b70b schema:location Berlin, Heidelberg
    43 schema:name Springer Berlin Heidelberg
    44 rdf:type schema:Organisation
    45 N4936c09b88e641dd8dfc431fca9d0a6e schema:name doi
    46 schema:value 10.1007/978-3-642-02716-1_6
    47 rdf:type schema:PropertyValue
    48 N7262e2bf59ae495d9d561604244a61cd rdf:first sg:person.014461136355.70
    49 rdf:rest Ned8414385d1c4bf6a161f869b8ee1b45
    50 N9956bd5608114c90ae2b742afc6e0bdc schema:familyName Waaler
    51 schema:givenName Arild
    52 rdf:type schema:Person
    53 Na000cf58ea8e410d95cbe1c6fd6d9da4 schema:name dimensions_id
    54 schema:value pub.1043408055
    55 rdf:type schema:PropertyValue
    56 Na30c78f6d29a41f89403a43e2155019c schema:isbn 978-3-642-02715-4
    57 978-3-642-02716-1
    58 schema:name Automated Reasoning with Analytic Tableaux and Related Methods
    59 rdf:type schema:Book
    60 Ne1131fa8bcdf4459ae4861f1dff55a8d rdf:first N9956bd5608114c90ae2b742afc6e0bdc
    61 rdf:rest rdf:nil
    62 Ne243188291524cb691a75f1f3a5c8f04 schema:name Springer Nature - SN SciGraph project
    63 rdf:type schema:Organization
    64 Ne6265c06e6b04c81870a53b8f905b05d schema:name readcube_id
    65 schema:value cec4c0dbb0759e2faf7c1ec5a0f96f738021a94004b808430caf40f127e4029b
    66 rdf:type schema:PropertyValue
    67 Ned8414385d1c4bf6a161f869b8ee1b45 rdf:first sg:person.011457433253.13
    68 rdf:rest rdf:nil
    69 anzsrc-for:08 schema:inDefinedTermSet anzsrc-for:
    70 schema:name Information and Computing Sciences
    71 rdf:type schema:DefinedTerm
    72 anzsrc-for:0801 schema:inDefinedTermSet anzsrc-for:
    73 schema:name Artificial Intelligence and Image Processing
    74 rdf:type schema:DefinedTerm
    75 sg:person.011457433253.13 schema:affiliation https://www.grid.ac/institutes/grid.12136.37
    76 schema:familyName Lahav
    77 schema:givenName Ori
    78 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.011457433253.13
    79 rdf:type schema:Person
    80 sg:person.014461136355.70 schema:affiliation https://www.grid.ac/institutes/grid.12136.37
    81 schema:familyName Avron
    82 schema:givenName Arnon
    83 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.014461136355.70
    84 rdf:type schema:Person
    85 sg:pub.10.1007/3-540-45744-5_45 schema:sameAs https://app.dimensions.ai/details/publication/pub.1051434466
    86 https://doi.org/10.1007/3-540-45744-5_45
    87 rdf:type schema:CreativeWork
    88 sg:pub.10.1007/978-94-017-0464-9_3 schema:sameAs https://app.dimensions.ai/details/publication/pub.1011250122
    89 https://doi.org/10.1007/978-94-017-0464-9_3
    90 rdf:type schema:CreativeWork
    91 sg:pub.10.1007/bf00881838 schema:sameAs https://app.dimensions.ai/details/publication/pub.1007496843
    92 https://doi.org/10.1007/bf00881838
    93 rdf:type schema:CreativeWork
    94 sg:pub.10.1007/s11225-005-8468-5 schema:sameAs https://app.dimensions.ai/details/publication/pub.1051156700
    95 https://doi.org/10.1007/s11225-005-8468-5
    96 rdf:type schema:CreativeWork
    97 sg:pub.10.1007/s11225-006-6607-2 schema:sameAs https://app.dimensions.ai/details/publication/pub.1007969950
    98 https://doi.org/10.1007/s11225-006-6607-2
    99 rdf:type schema:CreativeWork
    100 https://doi.org/10.1016/0890-5401(91)90023-u schema:sameAs https://app.dimensions.ai/details/publication/pub.1041008858
    101 rdf:type schema:CreativeWork
    102 https://doi.org/10.1016/j.apal.2008.09.015 schema:sameAs https://app.dimensions.ai/details/publication/pub.1008628061
    103 rdf:type schema:CreativeWork
    104 https://doi.org/10.1016/s0049-237x(08)71685-9 schema:sameAs https://app.dimensions.ai/details/publication/pub.1003546056
    105 rdf:type schema:CreativeWork
    106 https://doi.org/10.1093/logcom/exi001 schema:sameAs https://app.dimensions.ai/details/publication/pub.1059875940
    107 rdf:type schema:CreativeWork
    108 https://doi.org/10.2307/2271192 schema:sameAs https://app.dimensions.ai/details/publication/pub.1069855852
    109 rdf:type schema:CreativeWork
    110 https://www.grid.ac/institutes/grid.12136.37 schema:alternateName Tel Aviv University
    111 schema:name School of Computer Science, Tel-Aviv University, Israel
    112 rdf:type schema:Organization
     




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


    ...