Email Gateway (Jun 04 2025 at 13:38): Email Gateway (Jun 04 2025 at 13:38):From: Lawrence Paulson <lp15@cam.ac.uk>
I'm happy to announce a new entry:
A Verified Reduction Algorithm from MLSSmf to MLSS
by Yiran Duan and Lukas Stevens
Multi-level syllogistic with monotone functions (MLSSmf) is a sublanguage of set theory introduced by Cantone et al., involving set-to-set functions and their monotonicity, additivity, and multiplicativity. It is an extension of multi-level syllogistic with singleton (MLSS), which involves the predicates membership, set equality, set inclusion, and the operators union, intersection, set difference, and singleton. In this work we formalize the reduction algorithm from MLSSmf to MLSS and verify the correctness proof originally presented by Cantone et al. Combined with the verified decision procedure for MLSS formalized by Stevens, this yields an executable and verified decision procedure for MLSSmf.
https://www.isa-afp.org/entries/MLSSmf_to_MLSS.html
Last updated: Jun 20 2025 at 12:44 UTC