A Verified Reduction Algorithm from MLSSmf to MLSS (Q7361673)
From MaRDI portal
!
This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use the normal view instead:
AFP entry MLSSmf_to_MLSS
| Language | Label | Description | Also known as |
|---|---|---|---|
| default for all languages | No label defined |
||
| English | A Verified Reduction Algorithm from MLSSmf to MLSS |
AFP entry MLSSmf_to_MLSS |
Statements
5 May 2025
0 references
Yiran Duan
0 references
Lukas Stevens
0 references
A Verified Reduction Algorithm from MLSSmf to MLSS (English)
0 references
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 a verified decision procedure for MLSSmf .
0 references
