{"entities":{"Q7361037":{"pageid":31518650,"ns":120,"title":"Item:Q7361037","lastrevid":105362474,"modified":"2026-10-07T13:34:13Z","type":"item","id":"Q7361037","labels":{"en":{"language":"en","value":"A Comprehensive Framework for Saturation Theorem Proving"}},"descriptions":{"en":{"language":"en","value":"AFP entry Saturation_Framework"}},"aliases":{},"claims":{"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"72883fc399ee74c45f4566138cdc5df20cefa200","datavalue":{"value":"https://isa-afp.org/entries/Saturation_Framework.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q7361037$A6EA0934-73BD-4A30-A6BD-767D4277CB97","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"81ca710d57c429983a3babec89e140462b6a5857","datavalue":{"value":{"time":"+2020-04-09T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q7361037$433CE71D-710B-4B57-B73A-BB80CE9C81DD","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"8166375b6e885d78d9cc04a5e84d03f5f37dead4","datavalue":{"value":"Sophie Tourret","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361037$360AEA92-BA4F-4E7A-B0D1-408BAF9F00BC","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"be9014fa437db44c4909d16547279caa6e9a31a7","datavalue":{"value":{"text":"A Comprehensive Framework for Saturation Theorem Proving","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q7361037$DAACA11F-9133-4758-AD5C-57FBB0FF7406","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"d6c9e885024a15584f103ac2019b6533850cd148","datavalue":{"value":"This Isabelle/HOL formalization is the companion of the technical report \u201cA comprehensive framework for saturation theorem proving\u201d, itself companion of the eponym IJCAR 2020 paper, written by Uwe Waldmann, Sophie Tourret, Simon Robillard and Jasmin Blanchette. It verifies a framework for formal refutational completeness proofs of abstract provers that implement saturation calculi, such as ordered resolution or superposition, and allows to model entire prover architectures in such a way that the static refutational completeness of a calculus immediately implies the dynamic refutational completeness of a prover implementing the calculus using a variant of the given clause loop. The technical report \u201cA comprehensive framework for saturation theorem proving\u201d is available on the Matryoshka website . The names of the Isabelle lemmas and theorems corresponding to the results in the report are indicated in the margin of the report.","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361037$E618F288-91A4-4EAA-BB3F-D306F0380187","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":"Q7361037$7638FA58-0C45-453F-BF54-0D92F9557052","rank":"normal"}],"P585":[{"mainsnak":{"snaktype":"value","property":"P585","hash":"cd0c9d6eaf2232ef6bd24acb440211c3c1735214","datavalue":{"value":{"entity-type":"item","numeric-id":7361192,"id":"Q7361192"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361037$B1226230-97B2-4CEC-8656-80E05D58BD45","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P585","hash":"505db3695b4bfab8c374d45d12041cac811b0acf","datavalue":{"value":{"entity-type":"item","numeric-id":7361268,"id":"Q7361268"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361037$4DA0ECB5-778A-4427-96D4-74B5415F3822","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P585","hash":"96097fd8ad0239121f217726b3d18b7636f6739e","datavalue":{"value":{"entity-type":"item","numeric-id":7361640,"id":"Q7361640"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361037$B8A0E4B6-ED8B-444D-B8A3-07C19AB3E82A","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":"Q7361037$DAF0703B-7158-493B-A560-0D250B9A0136","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":"Q7361037$BE3CD634-66DA-436C-A3C4-AE9D3839734E","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"A Comprehensive Framework for Saturation Theorem Proving","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/A_Comprehensive_Framework_for_Saturation_Theorem_Proving"}}}}}