MLSS Decision Procedure (Q7361678)
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 MLSS_Decision_Proc
| Language | Label | Description | Also known as |
|---|---|---|---|
| default for all languages | No label defined |
||
| English | MLSS Decision Procedure |
AFP entry MLSS_Decision_Proc |
Statements
5 May 2023
0 references
Lukas Stevens
0 references
MLSS Decision Procedure (English)
0 references
This formalization verifies a decision procedure due to Cantone and Zarba for a quantifier-free fragment of set theory. The fragment is called multi-level syllogistic with singleton, or MLSS for short. Its syntax syntax includes the usual set operations union, intersection, difference, membership, equality as well as the construction of a set containing a single element. We specify the semantics of MLSS in terms of hereditarily finite sets and provide a sound and complete tableau calculus for it. We also provide an executable specification of a decision procedure that applies the rules of the calculus exhaustively and prove its termination. Furthermore, we extend the calculus with a light-weight type system that paves the way for an integration of the procedure into Isabelle/HOL.
0 references
