Nothing Special   »   [go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

A λ-unifiability test for set theory

  • Published:
Journal of Automated Reasoning Aims and scope Submit manuscript

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).

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

Explore related subjects

Discover the latest articles, news and stories from top researchers in related subjects.

References

  • Andrews, P. B., ‘Theorem proving via General Matings’, JACM 28 no. 2, pp. 193–214 (1981).

    Google Scholar 

  • Andrews, P. B. et al., ‘Automating Higher-order Logic,’ in Automated Theorem Proving: After 25 Years (ed. W. W. Bledsoe and D. Loveland), Contemporary Mathematics 29, pp. 169–192 (1984).

  • Bailin, S. C., ‘A Normalization Theorem for Set Theory,’ to appear in Journal of Symbolic Logic 53 no. 3, September 1988.

  • Huet, G. P., ‘A Unification Algorithm for Typed λ-Calculus,’ Theoretical Computer Science 1, pp. 27–57 (1974).

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Computer Technology Associates, Suite 201, 14900 Sweitzer Lane, 20707, Laurel, MD, USA

    Sidney C. Bailin

Authors
  1. Sidney C. Bailin
    View author publications

    You can also search for this author in PubMed Google Scholar

Additional information

This material is based upon work supported by the National Science Foundation under award number ISI-8560438. Any opinions, findings, and conclusions or recommendations expressed in this publication are those of the author and do not necessarily reflect the views of the National Science Foundation.

Rights and permissions

Reprints and permissions

About this article

Cite this article

Bailin, S.C. A λ-unifiability test for set theory. J Autom Reasoning 4, 269–286 (1988). https://doi.org/10.1007/BF00244943

Download citation

  • Received:

  • Issue Date:

  • DOI: https://doi.org/10.1007/BF00244943

Key words

Search

Navigation