{"entities":{"Q7361753":{"pageid":31520798,"ns":120,"title":"Item:Q7361753","lastrevid":105368852,"modified":"2026-10-07T13:37:39Z","type":"item","id":"Q7361753","labels":{"en":{"language":"en","value":"Extensions to the Comprehensive Framework for Saturation Theorem Proving"}},"descriptions":{"en":{"language":"en","value":"AFP entry Saturation_Framework_Extensions"}},"aliases":{},"claims":{"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"a1cfddbae1e57d983199e9b6c7d66178f84e6d2a","datavalue":{"value":"https://isa-afp.org/entries/Saturation_Framework_Extensions.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q7361753$6BC76535-84C0-4CC6-90B2-64FAE4878DCB","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"40d6298d979cc5fe8f26a1cea0e2ec254982529e","datavalue":{"value":{"time":"+2020-08-25T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q7361753$762A039A-3D0E-4B93-B36B-45A63A814A4D","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"d593b6f197721b1ecf9f17d8e5bbb2bb5a1f7f8a","datavalue":{"value":"Jasmin Christian Blanchette","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361753$1073A7DA-3DB6-4655-8EDF-453B7215D3C1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"8166375b6e885d78d9cc04a5e84d03f5f37dead4","datavalue":{"value":"Sophie Tourret","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361753$CCA01568-7A52-49BF-9BD3-26AE2D7BA6E3","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"93507e8d2fc16179fe3825e24b0221966a99c497","datavalue":{"value":{"text":"Extensions to the Comprehensive Framework for Saturation Theorem Proving","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q7361753$4F7C5274-5C1F-4E6B-BF51-32209F6E00A1","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"a94dd36756743992933e3fe6fe05cb196f43a338","datavalue":{"value":"This Isabelle/HOL formalization extends the AFP entry Saturation_Framework with the following contributions: an application of the framework to prove Bachmair and Ganzinger's resolution prover RP refutationally complete, which was formalized in a more ad hoc fashion by Schlichtkrull et al. in the AFP entry Ordered_Resultion_Prover ; generalizations of various basic concepts formalized by Schlichtkrull et al., which were needed to verify RP and could be useful to formalize other calculi, such as superposition; alternative proofs of fairness (and hence saturation and ultimately refutational completeness) for the given clause procedures GC and LGC, based on invariance.","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361753$A10BE5A2-7E00-48F1-83B3-EC2B2294AC8B","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":"Q7361753$645FA308-2A13-4544-8F91-329913FD36F2","rank":"normal"}],"P585":[{"mainsnak":{"snaktype":"value","property":"P585","hash":"6d228da4bce2fba997fec5a975b2ba853633b29e","datavalue":{"value":{"entity-type":"item","numeric-id":7361840,"id":"Q7361840"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361753$24D3EF68-6A4B-4996-9F14-714B424ECE40","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":"Q7361753$E670B7D3-CE80-4E73-923A-475DF82E3DF3","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":"Q7361753$4D0E8367-9708-409D-80E9-2407155D8724","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":"Q7361753$45650992-CFC7-4A9D-A96C-4E7EA5E9C7E7","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":"Q7361753$631D10EE-67F1-4E4E-92A2-615B036F022E","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":"Q7361753$0A69D507-FAA8-497B-B49A-D0BB196AB79E","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Extensions to the Comprehensive Framework for Saturation Theorem Proving","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Extensions_to_the_Comprehensive_Framework_for_Saturation_Theorem_Proving"}}}}}