{"entities":{"Q7361699":{"pageid":31520636,"ns":120,"title":"Item:Q7361699","lastrevid":105367307,"modified":"2026-10-07T13:36:46Z","type":"item","id":"Q7361699","labels":{"en":{"language":"en","value":"A Modular Formalization of Superposition"}},"descriptions":{"en":{"language":"en","value":"AFP entry Superposition_Calculus"}},"aliases":{},"claims":{"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"5e334be31da422efc4aec5337c15f28653fb9dbe","datavalue":{"value":"https://isa-afp.org/entries/Superposition_Calculus.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q7361699$7E12A9A5-EB5F-485B-9CEB-F6BE628D8B38","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"3e904a32ce9fe0905c581b0bf09991f7f3f0c6d0","datavalue":{"value":{"time":"+2024-10-24T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q7361699$A3CBCBA4-9EFA-4550-826F-61BF370EC0A5","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"e5724ef8b4ec23cf8c7c0feafb67eeb84d745382","datavalue":{"value":"Martin Desharnais-Sch\u00e4fer","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361699$DBD37808-CC89-40D5-9864-4745B5633334","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"15d203ac3247a8303c7b481047fdacbb38c8230e","datavalue":{"value":"Balazs Toth","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361699$53F0297E-423A-47C1-92CA-FA8FCD118791","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"9c9adf2d795fbd43ba7971a9a3c490c542067c0b","datavalue":{"value":{"text":"A Modular Formalization of Superposition","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q7361699$78A333F3-3A76-42C6-9E96-F8B84A06254F","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"c35af3b02102c37151877e4a0b19084dadd2d51e","datavalue":{"value":"Superposition is an efficient proof calculus for reasoning about first-order logic with equality that is implemented in many automatic theorem provers. It works by saturating the given set of clauses and is refutationally complete, meaning that if the set is inconsistent, the saturation will contain a contradiction. In this formalization, we restructured the completeness proof to cleanly separate the ground (i.e., variable-free) and nonground aspects. We relied on the IsaFoR library for first-order terms and on the Isabelle saturation framework. A paper describing this formalization was published at the 15th International Conference on Interactive Theorem Proving (ITP 2024).","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361699$DDF949E0-C280-4D5E-B5C0-3EAA735D73F2","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":"Q7361699$B2BBD6C3-281D-4948-B4E8-D25349FC97CD","rank":"normal"}],"P585":[{"mainsnak":{"snaktype":"value","property":"P585","hash":"f3da006a77785d92ace13f364fc1761aa09cf5d4","datavalue":{"value":{"entity-type":"item","numeric-id":7361364,"id":"Q7361364"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361699$1CFFF1D1-D2DA-4CD0-B121-EFACA023EBB7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P585","hash":"249de87d0640153f3160c5acaab414f3ad84be18","datavalue":{"value":{"entity-type":"item","numeric-id":7361037,"id":"Q7361037"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361699$D086A1A0-8CF0-40D6-990F-2D643DC0151B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P585","hash":"b9a61c696de92bdb09f875b4ad548670b0f0c015","datavalue":{"value":{"entity-type":"item","numeric-id":7361753,"id":"Q7361753"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361699$273BA878-5097-4D8F-B11E-1983E5A42D7F","rank":"normal"}],"P2651":[{"mainsnak":{"snaktype":"value","property":"P2651","hash":"fd4ac40fec1edeb460421a77e059cfe2df479821","datavalue":{"value":{"entity-type":"item","numeric-id":7360812,"id":"Q7360812"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361699$0F9B7C97-7ADA-408A-9ED0-6133BBA608F6","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":"Q7361699$66372C90-54AC-4348-A6D5-5287E5E96D02","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"A Modular Formalization of Superposition","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/A_Modular_Formalization_of_Superposition"}}}}}