A \(\lambda\)-unifiability test for set theory

DOI10.1007/BF00244943zbMath0715.03007OpenAlexW1551807233MaRDI QIDQ751644

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)

Related Items

Set theory for verification. I: From foundations to functions ⋮ \({\mathcal Z}\)-match: An inference rule for incrementally elaborating set instantiations