The undecidability of proof search when equality is a logical connective View Full Text


Ontology type: schema:ScholarlyArticle     


Article Info

DATE

2021-07-03

AUTHORS

Dale Miller, Alexandre Viel

ABSTRACT

One proof-theoretic approach to equality in quantificational logic treats equality as a logical connective: in particular, term equality can be given both left and right introduction rules in a sequent calculus proof system. We present a particular example of this approach to equality in a first-order logic setting in which there are no predicate symbols (apart from equality). After we illustrate some interesting applications of this logic, we show that provability in this logic is undecidable. More... »

PAGES

1-13

References to SciGraph publications

  • 2005. Hilbert’s Tenth Problem and Paradigms of Computation in NEW COMPUTATIONAL PARADIGMS
  • 2007-01-01. The Bedwyr System for Model Checking over Syntactic Expressions in AUTOMATED DEDUCTION – CADE-21
  • 1987. Intensional negation of logic programs: Examples and implementation techniques in TAPSOFT '87
  • 1993-02. A proof procedure for the logic of hereditary Harrop formulas in JOURNAL OF AUTOMATED REASONING
  • 1992-03. The Kreisel length-of-proof problem in ANNALS OF MATHEMATICS AND ARTIFICIAL INTELLIGENCE
  • 1994. Isabelle, A Generic Theorem Prover in NONE
  • 1988-03. The number of proof lines and the size of proofs in first order logic in ARCHIVE FOR MATHEMATICAL LOGIC
  • 2018-06-18. A Proof Theory for Model Checking in JOURNAL OF AUTOMATED REASONING
  • 1978. Negation as Failure in LOGIC AND DATA BASES
  • Identifiers

    URI

    http://scigraph.springernature.com/pub.10.1007/s10472-021-09764-0

    DOI

    http://dx.doi.org/10.1007/s10472-021-09764-0

    DIMENSIONS

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


    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/08", 
            "inDefinedTermSet": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/", 
            "name": "Information and Computing Sciences", 
            "type": "DefinedTerm"
          }, 
          {
            "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"
          }
        ], 
        "author": [
          {
            "affiliation": {
              "alternateName": "Inria Saclay & LIX/Ecole Polytechnique, 1 rue Honor\u00e9 d\u2019Estienne d\u2019Orves, 91120, Palaiseau, France", 
              "id": "http://www.grid.ac/institutes/grid.457355.5", 
              "name": [
                "Inria Saclay & LIX/Ecole Polytechnique, 1 rue Honor\u00e9 d\u2019Estienne d\u2019Orves, 91120, Palaiseau, France"
              ], 
              "type": "Organization"
            }, 
            "familyName": "Miller", 
            "givenName": "Dale", 
            "id": "sg:person.07476663267.12", 
            "sameAs": [
              "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.07476663267.12"
            ], 
            "type": "Person"
          }, 
          {
            "affiliation": {
              "alternateName": "Inria Saclay & LIX/Ecole Polytechnique, 1 rue Honor\u00e9 d\u2019Estienne d\u2019Orves, 91120, Palaiseau, France", 
              "id": "http://www.grid.ac/institutes/grid.457355.5", 
              "name": [
                "Inria Saclay & LIX/Ecole Polytechnique, 1 rue Honor\u00e9 d\u2019Estienne d\u2019Orves, 91120, Palaiseau, France"
              ], 
              "type": "Organization"
            }, 
            "familyName": "Viel", 
            "givenName": "Alexandre", 
            "type": "Person"
          }
        ], 
        "citation": [
          {
            "id": "sg:pub.10.1007/978-3-540-73595-3_28", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1034022743", 
              "https://doi.org/10.1007/978-3-540-73595-3_28"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/11494645_39", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1047667600", 
              "https://doi.org/10.1007/11494645_39"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/bfb0030541", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1109719027", 
              "https://doi.org/10.1007/bfb0030541"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/bf01531022", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1043505664", 
              "https://doi.org/10.1007/bf01531022"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/s10817-018-9475-3", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1104786650", 
              "https://doi.org/10.1007/s10817-018-9475-3"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/bf01625836", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1038370051", 
              "https://doi.org/10.1007/bf01625836"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/978-1-4684-3384-5_11", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1032205900", 
              "https://doi.org/10.1007/978-1-4684-3384-5_11"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/bf00881902", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1008249762", 
              "https://doi.org/10.1007/bf00881902"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/bfb0014975", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1041787247", 
              "https://doi.org/10.1007/bfb0014975"
            ], 
            "type": "CreativeWork"
          }
        ], 
        "datePublished": "2021-07-03", 
        "datePublishedReg": "2021-07-03", 
        "description": "One proof-theoretic approach to equality in quantificational logic treats equality as a logical connective: in particular, term equality can be given both left and right introduction rules in a sequent calculus proof system. We present a particular example of this approach to equality in a first-order logic setting in which there are no predicate symbols (apart from equality). After we illustrate some interesting applications of this logic, we show that provability in this logic is undecidable.", 
        "genre": "article", 
        "id": "sg:pub.10.1007/s10472-021-09764-0", 
        "inLanguage": "en", 
        "isAccessibleForFree": false, 
        "isPartOf": [
          {
            "id": "sg:journal.1043955", 
            "issn": [
              "1012-2443", 
              "1573-7470"
            ], 
            "name": "Annals of Mathematics and Artificial Intelligence", 
            "publisher": "Springer Nature", 
            "type": "Periodical"
          }
        ], 
        "keywords": [
          "logical connectives", 
          "term equality", 
          "introduction rules", 
          "equality", 
          "proof-theoretic approach", 
          "logic", 
          "first-order logic", 
          "predicate symbols", 
          "sequent calculus proof system", 
          "proof search", 
          "proof system", 
          "connectives", 
          "provability", 
          "particular example", 
          "undecidability", 
          "symbols", 
          "interesting applications", 
          "rules", 
          "approach", 
          "example", 
          "search", 
          "applications", 
          "system", 
          "quantificational logic treats equality", 
          "logic treats equality", 
          "treats equality", 
          "right introduction rules", 
          "calculus proof system"
        ], 
        "name": "The undecidability of proof search when equality is a logical connective", 
        "pagination": "1-13", 
        "productId": [
          {
            "name": "dimensions_id", 
            "type": "PropertyValue", 
            "value": [
              "pub.1139358942"
            ]
          }, 
          {
            "name": "doi", 
            "type": "PropertyValue", 
            "value": [
              "10.1007/s10472-021-09764-0"
            ]
          }
        ], 
        "sameAs": [
          "https://doi.org/10.1007/s10472-021-09764-0", 
          "https://app.dimensions.ai/details/publication/pub.1139358942"
        ], 
        "sdDataset": "articles", 
        "sdDatePublished": "2022-01-01T19:03", 
        "sdLicense": "https://scigraph.springernature.com/explorer/license/", 
        "sdPublisher": {
          "name": "Springer Nature - SN SciGraph project", 
          "type": "Organization"
        }, 
        "sdSource": "s3://com-springernature-scigraph/baseset/20220101/entities/gbq_results/article/article_912.jsonl", 
        "type": "ScholarlyArticle", 
        "url": "https://doi.org/10.1007/s10472-021-09764-0"
      }
    ]
     

    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/s10472-021-09764-0'

    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/s10472-021-09764-0'

    Turtle is a human-readable linked data format.

    curl -H 'Accept: text/turtle' 'https://scigraph.springernature.com/pub.10.1007/s10472-021-09764-0'

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

    curl -H 'Accept: application/rdf+xml' 'https://scigraph.springernature.com/pub.10.1007/s10472-021-09764-0'


     

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

    122 TRIPLES      22 PREDICATES      60 URIs      43 LITERALS      4 BLANK NODES

    Subject Predicate Object
    1 sg:pub.10.1007/s10472-021-09764-0 schema:about anzsrc-for:08
    2 anzsrc-for:0802
    3 schema:author N5b4e7d93279a4b0a9839ad25be941413
    4 schema:citation sg:pub.10.1007/11494645_39
    5 sg:pub.10.1007/978-1-4684-3384-5_11
    6 sg:pub.10.1007/978-3-540-73595-3_28
    7 sg:pub.10.1007/bf00881902
    8 sg:pub.10.1007/bf01531022
    9 sg:pub.10.1007/bf01625836
    10 sg:pub.10.1007/bfb0014975
    11 sg:pub.10.1007/bfb0030541
    12 sg:pub.10.1007/s10817-018-9475-3
    13 schema:datePublished 2021-07-03
    14 schema:datePublishedReg 2021-07-03
    15 schema:description One proof-theoretic approach to equality in quantificational logic treats equality as a logical connective: in particular, term equality can be given both left and right introduction rules in a sequent calculus proof system. We present a particular example of this approach to equality in a first-order logic setting in which there are no predicate symbols (apart from equality). After we illustrate some interesting applications of this logic, we show that provability in this logic is undecidable.
    16 schema:genre article
    17 schema:inLanguage en
    18 schema:isAccessibleForFree false
    19 schema:isPartOf sg:journal.1043955
    20 schema:keywords applications
    21 approach
    22 calculus proof system
    23 connectives
    24 equality
    25 example
    26 first-order logic
    27 interesting applications
    28 introduction rules
    29 logic
    30 logic treats equality
    31 logical connectives
    32 particular example
    33 predicate symbols
    34 proof search
    35 proof system
    36 proof-theoretic approach
    37 provability
    38 quantificational logic treats equality
    39 right introduction rules
    40 rules
    41 search
    42 sequent calculus proof system
    43 symbols
    44 system
    45 term equality
    46 treats equality
    47 undecidability
    48 schema:name The undecidability of proof search when equality is a logical connective
    49 schema:pagination 1-13
    50 schema:productId N177e7a5f6cfa4e1f94a16b1fbcfb800c
    51 N6e4833ba85ec4f6eb181e417c889880e
    52 schema:sameAs https://app.dimensions.ai/details/publication/pub.1139358942
    53 https://doi.org/10.1007/s10472-021-09764-0
    54 schema:sdDatePublished 2022-01-01T19:03
    55 schema:sdLicense https://scigraph.springernature.com/explorer/license/
    56 schema:sdPublisher N00a6caae2e0a485f9c2a70e3431a4ea0
    57 schema:url https://doi.org/10.1007/s10472-021-09764-0
    58 sgo:license sg:explorer/license/
    59 sgo:sdDataset articles
    60 rdf:type schema:ScholarlyArticle
    61 N00a6caae2e0a485f9c2a70e3431a4ea0 schema:name Springer Nature - SN SciGraph project
    62 rdf:type schema:Organization
    63 N177e7a5f6cfa4e1f94a16b1fbcfb800c schema:name doi
    64 schema:value 10.1007/s10472-021-09764-0
    65 rdf:type schema:PropertyValue
    66 N5b4e7d93279a4b0a9839ad25be941413 rdf:first sg:person.07476663267.12
    67 rdf:rest Nf0e357bcce7840cb9b38099c3aad7b1c
    68 N6e4833ba85ec4f6eb181e417c889880e schema:name dimensions_id
    69 schema:value pub.1139358942
    70 rdf:type schema:PropertyValue
    71 N8611f4d2631e427f88f55e923c68c611 schema:affiliation grid-institutes:grid.457355.5
    72 schema:familyName Viel
    73 schema:givenName Alexandre
    74 rdf:type schema:Person
    75 Nf0e357bcce7840cb9b38099c3aad7b1c rdf:first N8611f4d2631e427f88f55e923c68c611
    76 rdf:rest rdf:nil
    77 anzsrc-for:08 schema:inDefinedTermSet anzsrc-for:
    78 schema:name Information and Computing Sciences
    79 rdf:type schema:DefinedTerm
    80 anzsrc-for:0802 schema:inDefinedTermSet anzsrc-for:
    81 schema:name Computation Theory and Mathematics
    82 rdf:type schema:DefinedTerm
    83 sg:journal.1043955 schema:issn 1012-2443
    84 1573-7470
    85 schema:name Annals of Mathematics and Artificial Intelligence
    86 schema:publisher Springer Nature
    87 rdf:type schema:Periodical
    88 sg:person.07476663267.12 schema:affiliation grid-institutes:grid.457355.5
    89 schema:familyName Miller
    90 schema:givenName Dale
    91 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.07476663267.12
    92 rdf:type schema:Person
    93 sg:pub.10.1007/11494645_39 schema:sameAs https://app.dimensions.ai/details/publication/pub.1047667600
    94 https://doi.org/10.1007/11494645_39
    95 rdf:type schema:CreativeWork
    96 sg:pub.10.1007/978-1-4684-3384-5_11 schema:sameAs https://app.dimensions.ai/details/publication/pub.1032205900
    97 https://doi.org/10.1007/978-1-4684-3384-5_11
    98 rdf:type schema:CreativeWork
    99 sg:pub.10.1007/978-3-540-73595-3_28 schema:sameAs https://app.dimensions.ai/details/publication/pub.1034022743
    100 https://doi.org/10.1007/978-3-540-73595-3_28
    101 rdf:type schema:CreativeWork
    102 sg:pub.10.1007/bf00881902 schema:sameAs https://app.dimensions.ai/details/publication/pub.1008249762
    103 https://doi.org/10.1007/bf00881902
    104 rdf:type schema:CreativeWork
    105 sg:pub.10.1007/bf01531022 schema:sameAs https://app.dimensions.ai/details/publication/pub.1043505664
    106 https://doi.org/10.1007/bf01531022
    107 rdf:type schema:CreativeWork
    108 sg:pub.10.1007/bf01625836 schema:sameAs https://app.dimensions.ai/details/publication/pub.1038370051
    109 https://doi.org/10.1007/bf01625836
    110 rdf:type schema:CreativeWork
    111 sg:pub.10.1007/bfb0014975 schema:sameAs https://app.dimensions.ai/details/publication/pub.1041787247
    112 https://doi.org/10.1007/bfb0014975
    113 rdf:type schema:CreativeWork
    114 sg:pub.10.1007/bfb0030541 schema:sameAs https://app.dimensions.ai/details/publication/pub.1109719027
    115 https://doi.org/10.1007/bfb0030541
    116 rdf:type schema:CreativeWork
    117 sg:pub.10.1007/s10817-018-9475-3 schema:sameAs https://app.dimensions.ai/details/publication/pub.1104786650
    118 https://doi.org/10.1007/s10817-018-9475-3
    119 rdf:type schema:CreativeWork
    120 grid-institutes:grid.457355.5 schema:alternateName Inria Saclay & LIX/Ecole Polytechnique, 1 rue Honoré d’Estienne d’Orves, 91120, Palaiseau, France
    121 schema:name Inria Saclay & LIX/Ecole Polytechnique, 1 rue Honoré d’Estienne d’Orves, 91120, Palaiseau, France
    122 rdf:type schema:Organization
     




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


    ...