A -unifiability test for set theory

DOI10.1007/BF00244943MaRDI QIDQ751644zbMATH OpenOpenAlexFDO

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

Recommendations

• scientific article; zbMATH DE number 1303341
• scientific article; zbMATH DE number 3935004
• Publication:4506398
• Semi-unification
• Set unification

Cited in

(7)

• Towards the range property for the lambda theory \(\mathcal H\)
• scientific article; zbMATH DE number 3935004 (Why is no real title available?)
• Set theory for verification. I: From foundations to functions
• The infinity Lambda test: A multi-dimensional version of Banerjee infinity test
• \({\mathcal Z}\)-match: An inference rule for incrementally elaborating set instantiations
• scientific article; zbMATH DE number 4068831 (Why is no real title available?)
• scientific article; zbMATH DE number 516996 (Why is no real title available?)

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)