{"entities":{"Q7361910":{"pageid":31521269,"ns":120,"title":"Item:Q7361910","lastrevid":105370289,"modified":"2026-10-07T13:39:08Z","type":"item","id":"Q7361910","labels":{"en":{"language":"en","value":"A Modular Splitting Framework for Saturation Theorem Proving"}},"descriptions":{"en":{"language":"en","value":"AFP entry Splitting_Framework"}},"aliases":{},"claims":{"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"62b7370680cff8329b1246fb321679e7d6c5c0ac","datavalue":{"value":"https://isa-afp.org/entries/Splitting_Framework.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q7361910$3834DAD9-3577-4CEF-A762-AE35452360BB","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"66c9695eb20dc9e6bcc46cab6b3e0d2faaff014c","datavalue":{"value":{"time":"+2025-06-18T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q7361910$80D9CE69-0B6F-449F-BD0B-30FAF1EF57C0","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"12ed347a68809a7f07ed9cbc1b2146beee77f087","datavalue":{"value":"Ghilain Bergeron","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361910$900E325A-5052-46F2-A42E-100906B2790D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"e2798dd97595db995fbe9b9a5f6f1dffb77e7a12","datavalue":{"value":"Florent Krasnopol","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361910$68579330-B6B2-475F-9DFE-6C9F02FB0855","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"8166375b6e885d78d9cc04a5e84d03f5f37dead4","datavalue":{"value":"Sophie Tourret","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361910$C9500EBC-1EA8-472D-9DB7-D8C4FF74FC28","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"2e4c382ba51dfcf260ec789ccd0f0411b0960fe6","datavalue":{"value":{"text":"A Modular Splitting Framework for Saturation Theorem Proving","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q7361910$0F1F698F-3DFD-4C1E-ADB9-B4011BAD2C83","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"6428711b8953661b7f4d5757a3df0cdf3c1af47f","datavalue":{"value":"We formalize in Isabelle/HOL a framework for splitting, a theorem proving technique that extends saturation-based calculi with branching abilities. The framework preserves the completeness of the original calculus. We focus here on the simplest splitting model described in details in the first three sections of \"Unifying Splitting\" by Gabriel Ebner, Jasmin Blanchette and Sophie Tourret and provide an extension of the ordered resolution calculus with a variant of splitting called Lightweight AVATAR. A paper describing the present formalization has been accepted at ITP'25.","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361910$11A3058C-758E-44B6-8BF8-D0B6CF95EB3B","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"1b2a91de7958ff661b361ca2244230738e017656","datavalue":{"value":{"entity-type":"item","numeric-id":7323672,"id":"Q7323672"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361910$83AC676B-42E6-4F18-A02C-7B7451BC71DB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"33f8e1ec7fbedbd73ef97a55912f6e62728ba139","datavalue":{"value":{"entity-type":"item","numeric-id":2055869,"id":"Q2055869"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361910$8436BB27-573E-4794-82E2-B61F42DBE1BF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"df86a0ed10db66a7e1f365b05afe861b77934d95","datavalue":{"value":{"entity-type":"item","numeric-id":6103590,"id":"Q6103590"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361910$A57AF8A7-0789-452F-983A-4F8604BE078B","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":"Q7361910$9EF8B791-EFB3-4496-BA31-58343C26AC2C","rank":"normal"}],"P585":[{"mainsnak":{"snaktype":"value","property":"P585","hash":"6603b2a587424388be085eadb1b94d7144f1c3de","datavalue":{"value":{"entity-type":"item","numeric-id":7361652,"id":"Q7361652"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361910$35DEA9A9-ECD2-417A-94AA-5FAD980E0987","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":"Q7361910$C054024D-E834-4E69-93BF-9040AE0C17E1","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":"Q7361910$719F34F5-C07A-4A5E-ADA2-E0533F718AEC","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":"Q7361910$473D2511-FD2B-410C-A5D7-BC3839DF226B","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":"Q7361910$94D35849-62E5-4CC0-8D41-A49BEB2706DA","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"A Modular Splitting Framework for Saturation Theorem Proving","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/A_Modular_Splitting_Framework_for_Saturation_Theorem_Proving"}}}}}