{"entities":{"Q7361678":{"pageid":31520573,"ns":120,"title":"Item:Q7361678","lastrevid":105367061,"modified":"2026-10-07T13:36:44Z","type":"item","id":"Q7361678","labels":{"en":{"language":"en","value":"MLSS Decision Procedure"}},"descriptions":{"en":{"language":"en","value":"AFP entry MLSS_Decision_Proc"}},"aliases":{},"claims":{"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"bc36748148b59fc0e5d7df3b06bcd9b299421094","datavalue":{"value":"https://isa-afp.org/entries/MLSS_Decision_Proc.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q7361678$2318CF03-8B0C-4E1A-AF88-05AB3A0FA8AB","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"5a9ffdd3d0278110160d03bdc1ac988576aaeda7","datavalue":{"value":{"time":"+2023-05-05T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q7361678$CDF078E8-95B5-4AD3-8EFD-1C8359BD8883","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"4e98f0231411584171b7068266a9aef8929eef72","datavalue":{"value":"Lukas Stevens","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361678$3ACD04F0-96BD-46E9-8C53-DF27D2D0C2CD","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"d6c1a614f312c5b47b5b90a9dd91499935f12f77","datavalue":{"value":{"text":"MLSS Decision Procedure","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q7361678$EDF97051-17B3-4C69-8E5E-642E07A28F7A","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"953d4b4d1a62a89abf2fe1d209a5ffb815b9ae9e","datavalue":{"value":"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.","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361678$6BD4B9BC-4DE5-4F95-947F-5AD0DCCE22C7","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"caaa4b84c8d83da8bae05dbdfffe44e7c6e954fc","datavalue":{"value":{"entity-type":"item","numeric-id":4503906,"id":"Q4503906"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361678$3AF75EBB-48DF-4AC6-AA45-E1B02102B2BB","rank":"normal"}],"P37":[{"mainsnak":{"snaktype":"value","property":"P37","hash":"9a21a8eebe97539644aa32b24dda137c12e751dc","datavalue":{"value":{"entity-type":"item","numeric-id":40327,"id":"Q40327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361678$888CBD32-675F-4CB5-91DB-F350DCD824C5","rank":"normal"}],"P585":[{"mainsnak":{"snaktype":"value","property":"P585","hash":"c7a8f6bee75646b3f0253f9b38a1467a1e90950c","datavalue":{"value":{"entity-type":"item","numeric-id":7361712,"id":"Q7361712"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361678$47835FE2-A889-4F71-986C-02438AC23DE1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P585","hash":"b999678a517221bed9bd614caca8006ebca3a529","datavalue":{"value":{"entity-type":"item","numeric-id":7361796,"id":"Q7361796"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361678$A2F71016-6F13-4013-8BBC-8DEE57C5FBF7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P585","hash":"76069a6d59279efa1dd2eb6eeafe6968fbde0cc3","datavalue":{"value":{"entity-type":"item","numeric-id":7361169,"id":"Q7361169"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361678$589B2308-967F-43D0-9AA6-0B4B80B1EE2C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P585","hash":"e0b5465b6a0d9e05645cdb7168eee1aaf7eb2845","datavalue":{"value":{"entity-type":"item","numeric-id":7361518,"id":"Q7361518"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361678$4FDAEDA6-2B3C-48AE-8FAB-97334609FE51","rank":"normal"}],"P2651":[{"mainsnak":{"snaktype":"value","property":"P2651","hash":"46a3c16c7f23b7b076a59467a678c276f115551a","datavalue":{"value":{"entity-type":"item","numeric-id":7360809,"id":"Q7360809"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361678$5BB930A7-FB24-4FD4-8F38-688A79A13121","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P2651","hash":"017b24027bc3172f77cd322e56e3cf55676e8403","datavalue":{"value":{"entity-type":"item","numeric-id":7360810,"id":"Q7360810"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361678$FE941A9A-3322-4661-B83D-2F71E291B668","rank":"normal"}],"P1460":[{"mainsnak":{"snaktype":"value","property":"P1460","hash":"908c3454b3659c4b140ccce33c5aee31081edc8d","datavalue":{"value":{"entity-type":"item","numeric-id":5976450,"id":"Q5976450"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361678$880E0665-D802-4C85-9FF1-7FFFF0B09229","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"MLSS Decision Procedure","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/MLSS_Decision_Procedure"}}}}}