A \(\lambda\)-unifiability test for set theory
From MaRDI portal
Publication:751644
DOI10.1007/BF00244943zbMath0715.03007OpenAlexW1551807233MaRDI QIDQ751644
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
\(\lambda \) -unificationAda-like pseudocodelambda-contractionsemi-decision algorithm for the unifiability of two set-theoretic formulas modulo \(\lambda \) -reduction
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