A λ-unifiability test for set theory View Full Text


Ontology type: schema:ScholarlyArticle     


Article Info

DATE

1988-09

AUTHORS

Sidney C. Bailin

ABSTRACT

We present a semi-decision algorithm for the unifiability of two set-theoretic formulas modulo λ-reduction. The algorithm is based on the approach developed by G. Huet for type theory, but requires additional measures because formulas in set theory are not all normalizable. We present the algorithm in an Ada-like pseudocode, and then prove two theorems that show the completeness and correctness of the procedure. We conclude by showing that λ-unification is not a complete quantifier substitution method for set theory-unlile first-order unification and first-order logic. In this respect set theory is similar to type theory (higher-order logic). More... »

PAGES

269-286

Identifiers

URI

http://scigraph.springernature.com/pub.10.1007/bf00244943

DOI

http://dx.doi.org/10.1007/bf00244943

DIMENSIONS

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


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/17", 
        "inDefinedTermSet": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/", 
        "name": "Psychology and Cognitive Sciences", 
        "type": "DefinedTerm"
      }, 
      {
        "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/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/1702", 
        "inDefinedTermSet": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/", 
        "name": "Cognitive Sciences", 
        "type": "DefinedTerm"
      }
    ], 
    "author": [
      {
        "affiliation": {
          "alternateName": "Computer Technology Associates, Suite 201, 14900 Sweitzer Lane, 20707, Laurel, MD, USA", 
          "id": "http://www.grid.ac/institutes/grid.433150.0", 
          "name": [
            "Computer Technology Associates, Suite 201, 14900 Sweitzer Lane, 20707, Laurel, MD, USA"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Bailin", 
        "givenName": "Sidney C.", 
        "id": "sg:person.011667755735.32", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.011667755735.32"
        ], 
        "type": "Person"
      }
    ], 
    "datePublished": "1988-09", 
    "datePublishedReg": "1988-09-01", 
    "description": "We present a semi-decision algorithm for the unifiability of two set-theoretic formulas modulo \u03bb-reduction. The algorithm is based on the approach developed by G. Huet for type theory, but requires additional measures because formulas in set theory are not all normalizable. We present the algorithm in an Ada-like pseudocode, and then prove two theorems that show the completeness and correctness of the procedure. We conclude by showing that \u03bb-unification is not a complete quantifier substitution method for set theory-unlile first-order unification and first-order logic. In this respect set theory is similar to type theory (higher-order logic).", 
    "genre": "article", 
    "id": "sg:pub.10.1007/bf00244943", 
    "inLanguage": "en", 
    "isAccessibleForFree": false, 
    "isPartOf": [
      {
        "id": "sg:journal.1136522", 
        "issn": [
          "0168-7433", 
          "1573-0670"
        ], 
        "name": "Journal of Automated Reasoning", 
        "publisher": "Springer Nature", 
        "type": "Periodical"
      }, 
      {
        "issueNumber": "3", 
        "type": "PublicationIssue"
      }, 
      {
        "type": "PublicationVolume", 
        "volumeNumber": "4"
      }
    ], 
    "keywords": [
      "type theory", 
      "first-order logic", 
      "theory", 
      "set theory", 
      "unification", 
      "unifiability", 
      "Huet", 
      "logic", 
      "respect", 
      "approach", 
      "completeness", 
      "additional measures", 
      "correctness", 
      "algorithm", 
      "measures", 
      "formula", 
      "theorem", 
      "procedure", 
      "substitution method", 
      "method", 
      "semi-decision algorithm", 
      "pseudocode", 
      "first-order unification", 
      "reduction", 
      "test"
    ], 
    "name": "A \u03bb-unifiability test for set theory", 
    "pagination": "269-286", 
    "productId": [
      {
        "name": "dimensions_id", 
        "type": "PropertyValue", 
        "value": [
          "pub.1017454428"
        ]
      }, 
      {
        "name": "doi", 
        "type": "PropertyValue", 
        "value": [
          "10.1007/bf00244943"
        ]
      }
    ], 
    "sameAs": [
      "https://doi.org/10.1007/bf00244943", 
      "https://app.dimensions.ai/details/publication/pub.1017454428"
    ], 
    "sdDataset": "articles", 
    "sdDatePublished": "2022-06-01T21:59", 
    "sdLicense": "https://scigraph.springernature.com/explorer/license/", 
    "sdPublisher": {
      "name": "Springer Nature - SN SciGraph project", 
      "type": "Organization"
    }, 
    "sdSource": "s3://com-springernature-scigraph/baseset/20220601/entities/gbq_results/article/article_193.jsonl", 
    "type": "ScholarlyArticle", 
    "url": "https://doi.org/10.1007/bf00244943"
  }
]
 

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/bf00244943'

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/bf00244943'

Turtle is a human-readable linked data format.

curl -H 'Accept: text/turtle' 'https://scigraph.springernature.com/pub.10.1007/bf00244943'

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

curl -H 'Accept: application/rdf+xml' 'https://scigraph.springernature.com/pub.10.1007/bf00244943'


 

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

95 TRIPLES      21 PREDICATES      54 URIs      43 LITERALS      6 BLANK NODES

Subject Predicate Object
1 sg:pub.10.1007/bf00244943 schema:about anzsrc-for:08
2 anzsrc-for:0801
3 anzsrc-for:0802
4 anzsrc-for:17
5 anzsrc-for:1702
6 schema:author Nb86c2e41af664c9c8d3f0cd94c3bfedb
7 schema:datePublished 1988-09
8 schema:datePublishedReg 1988-09-01
9 schema:description We present a semi-decision algorithm for the unifiability of two set-theoretic formulas modulo λ-reduction. The algorithm is based on the approach developed by G. Huet for type theory, but requires additional measures because formulas in set theory are not all normalizable. We present the algorithm in an Ada-like pseudocode, and then prove two theorems that show the completeness and correctness of the procedure. We conclude by showing that λ-unification is not a complete quantifier substitution method for set theory-unlile first-order unification and first-order logic. In this respect set theory is similar to type theory (higher-order logic).
10 schema:genre article
11 schema:inLanguage en
12 schema:isAccessibleForFree false
13 schema:isPartOf N102c613649ec4c0c96f0b65bb4de2d98
14 Na6ca7cefecf146e29cca349fe44ca104
15 sg:journal.1136522
16 schema:keywords Huet
17 additional measures
18 algorithm
19 approach
20 completeness
21 correctness
22 first-order logic
23 first-order unification
24 formula
25 logic
26 measures
27 method
28 procedure
29 pseudocode
30 reduction
31 respect
32 semi-decision algorithm
33 set theory
34 substitution method
35 test
36 theorem
37 theory
38 type theory
39 unifiability
40 unification
41 schema:name A λ-unifiability test for set theory
42 schema:pagination 269-286
43 schema:productId N80759ffab73f4960b0ae443b3f8cf7b2
44 N913f70aa021f402ab691a44cdf2bed8c
45 schema:sameAs https://app.dimensions.ai/details/publication/pub.1017454428
46 https://doi.org/10.1007/bf00244943
47 schema:sdDatePublished 2022-06-01T21:59
48 schema:sdLicense https://scigraph.springernature.com/explorer/license/
49 schema:sdPublisher N07243363c61b49758860d1f04468cb7d
50 schema:url https://doi.org/10.1007/bf00244943
51 sgo:license sg:explorer/license/
52 sgo:sdDataset articles
53 rdf:type schema:ScholarlyArticle
54 N07243363c61b49758860d1f04468cb7d schema:name Springer Nature - SN SciGraph project
55 rdf:type schema:Organization
56 N102c613649ec4c0c96f0b65bb4de2d98 schema:issueNumber 3
57 rdf:type schema:PublicationIssue
58 N80759ffab73f4960b0ae443b3f8cf7b2 schema:name dimensions_id
59 schema:value pub.1017454428
60 rdf:type schema:PropertyValue
61 N913f70aa021f402ab691a44cdf2bed8c schema:name doi
62 schema:value 10.1007/bf00244943
63 rdf:type schema:PropertyValue
64 Na6ca7cefecf146e29cca349fe44ca104 schema:volumeNumber 4
65 rdf:type schema:PublicationVolume
66 Nb86c2e41af664c9c8d3f0cd94c3bfedb rdf:first sg:person.011667755735.32
67 rdf:rest rdf:nil
68 anzsrc-for:08 schema:inDefinedTermSet anzsrc-for:
69 schema:name Information and Computing Sciences
70 rdf:type schema:DefinedTerm
71 anzsrc-for:0801 schema:inDefinedTermSet anzsrc-for:
72 schema:name Artificial Intelligence and Image Processing
73 rdf:type schema:DefinedTerm
74 anzsrc-for:0802 schema:inDefinedTermSet anzsrc-for:
75 schema:name Computation Theory and Mathematics
76 rdf:type schema:DefinedTerm
77 anzsrc-for:17 schema:inDefinedTermSet anzsrc-for:
78 schema:name Psychology and Cognitive Sciences
79 rdf:type schema:DefinedTerm
80 anzsrc-for:1702 schema:inDefinedTermSet anzsrc-for:
81 schema:name Cognitive Sciences
82 rdf:type schema:DefinedTerm
83 sg:journal.1136522 schema:issn 0168-7433
84 1573-0670
85 schema:name Journal of Automated Reasoning
86 schema:publisher Springer Nature
87 rdf:type schema:Periodical
88 sg:person.011667755735.32 schema:affiliation grid-institutes:grid.433150.0
89 schema:familyName Bailin
90 schema:givenName Sidney C.
91 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.011667755735.32
92 rdf:type schema:Person
93 grid-institutes:grid.433150.0 schema:alternateName Computer Technology Associates, Suite 201, 14900 Sweitzer Lane, 20707, Laurel, MD, USA
94 schema:name Computer Technology Associates, Suite 201, 14900 Sweitzer Lane, 20707, Laurel, MD, USA
95 rdf:type schema:Organization
 




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


...