A -unifiability test for set theory

DOI10.1007/BF00244943zbMATH Open0715.03007OpenAlexW1551807233MaRDI QIDQ751644FDOQ751644

Sidney C. Bailin

Publication date: 1988

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/bf00244943

zbMATH Keywords

\(\lambda \) -unificationAda-like pseudocodelambda-contractionsemi-decision algorithm for the unifiability of two set-theoretic formulas modulo \(\lambda \) -reduction

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Software, source code, etc. for problems pertaining to mathematical logic and foundations (03-04)

Cited In (5)

• Title not available (Why is that?)
• Set theory for verification. I: From foundations to functions
• \({\mathcal Z}\)-match: An inference rule for incrementally elaborating set instantiations
• Towards the range property for the lambda theory \(\mathcal H\)
• The infinity Lambda test: A multi-dimensional version of Banerjee infinity test

   Recommendations

• Title not available (Why is that?) 👍 👎
• Title not available (Why is that?) 👍 👎
• Title not available (Why is that?) 👍 👎
• Semi-unification 👍 👎
• Set unification 👍 👎

This page was built for publication: A \(\lambda\)-unifiability test for set theory

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q751644)