{"entities":{"Q7361268":{"pageid":31519343,"ns":120,"title":"Item:Q7361268","lastrevid":105423494,"modified":"2026-10-08T13:45:25Z","type":"item","id":"Q7361268","labels":{"en":{"language":"en","value":"Formalization of Bachmair and Ganzinger's Ordered Resolution Prover"}},"descriptions":{"en":{"language":"en","value":"AFP entry Ordered_Resolution_Prover"}},"aliases":{},"claims":{"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"b77b6c593a86cb9d6829a802357cae8330647faa","datavalue":{"value":"https://isa-afp.org/entries/Ordered_Resolution_Prover.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q7361268$A77845F9-32E9-4A13-8800-915EC6337638","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"f19e42813e41b1b694ee6662dce0e445e8e41f4b","datavalue":{"value":"Anders Schlichtkrull","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361268$15003D21-D6D9-4890-BED3-2748A0E6ED23","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"d593b6f197721b1ecf9f17d8e5bbb2bb5a1f7f8a","datavalue":{"value":"Jasmin Christian Blanchette","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361268$9420B71E-E586-4B2D-B005-32C6140007B7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"2500aa80beaafa12dfa4ab6c7d8363674f762e6e","datavalue":{"value":"Dmitriy Traytel","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361268$4A5CAF08-5E81-450D-BC6A-875941AEF0A8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"0bea28856612bb879f597a9d9f573ece274a0783","datavalue":{"value":"Uwe Waldmann","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361268$C08D61AF-C104-4CA6-8C8D-EB6781E9A540","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"37a2d97e15ccb2cd6eb1d448b7caa75fada9d10a","datavalue":{"value":"This Isabelle/HOL formalization covers Sections 2 to 4 of Bachmair and Ganzinger's \"Resolution Theorem Proving\" chapter in the Handbook of Automated Reasoning . This includes soundness and completeness of unordered and ordered variants of ground resolution with and without literal selection, the standard redundancy criterion, a general framework for refutational theorem proving, and soundness and completeness of an abstract first-order prover.","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361268$61FAEFEE-3276-45B1-B86D-11026E700EE3","rank":"normal"}],"P585":[{"mainsnak":{"snaktype":"value","property":"P585","hash":"c9d73c02403c0af647a73b8da7299dbef78ebf0b","datavalue":{"value":{"entity-type":"item","numeric-id":7361764,"id":"Q7361764"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361268$C0C80823-56FC-40E6-8950-8BE5C52C9F38","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P585","hash":"8f0f13c41ff97fc90cd117120ced19e3dd24a1b3","datavalue":{"value":{"entity-type":"item","numeric-id":7361305,"id":"Q7361305"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361268$9FDF0C62-A39E-4553-BAEA-5246019ADB82","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"2870c2a89ad093911e8a3011d1a5f8b51084c5a2","datavalue":{"value":{"time":"+2018-01-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":"Q7361268$ECC10F8F-7173-4154-9080-9F63C025B92F","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"d88bb946208cffa5a51d7def81ddaa827da783e7","datavalue":{"value":{"text":"Formalization of Bachmair and Ganzinger's Ordered Resolution Prover","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q7361268$7E3ECCBC-6845-4655-98D3-1E2A63CD5A4E","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":"Q7361268$3F92DDFC-3E08-470C-9F39-D8CE8704AD7D","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":"Q7361268$1E83EB58-F652-41F3-958D-6661187EFC84","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":"Q7361268$82BEB58A-BC77-4E20-9322-B98DEF535104","rank":"normal"}],"P13":[{"mainsnak":{"snaktype":"value","property":"P13","hash":"0c1cc967e825a90ea00b878af0be1c66d00e5062","datavalue":{"value":"38028","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q7361268$FEE541BB-116A-48CF-9B76-2BE23C4CA083","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"9ccfc2ffdb7a60cd36d8dca0a4e6d9d45f5228f3","datavalue":{"value":"3","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q7361268$B444D774-7FF3-46AB-B1FE-15FC892E5D7F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"09f5e0c6033338f59ef27e37d6877da0f26d9646","datavalue":{"value":"68.0","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q7361268$F484D133-2083-40F9-B596-41C595E1FA0C","rank":"normal"}],"P286":[{"mainsnak":{"snaktype":"value","property":"P286","hash":"777bd9001c7d49fa6c1e0b184094fdcf5f8073e8","datavalue":{"value":{"entity-type":"item","numeric-id":5919011,"id":"Q5919011"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361268$907201E2-01C4-4EA8-BF07-AD3DFC15632E","rank":"normal"}],"P1458":[{"mainsnak":{"snaktype":"value","property":"P1458","hash":"bb05cb23794774f62a8e4aa4de610af231973a1d","datavalue":{"value":{"entity-type":"item","numeric-id":40327,"id":"Q40327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361268$A0F08E20-9413-439F-8212-5D098E06FE9F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"a2a767ccd0e9bdc5b1b4a2069a6679f9340a857a","datavalue":{"value":{"entity-type":"item","numeric-id":14275,"id":"Q14275"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361268$EC76B81D-FF19-4661-AB5A-F19D63A4BDE5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"28fc316ccc1f38bd6830fcffe3187b6d32168084","datavalue":{"value":{"entity-type":"item","numeric-id":15455,"id":"Q15455"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361268$28B30C84-EB9F-426B-87A8-AFE857139E7C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"ed15eb8701a335444fde1bcc3327d1067ce64751","datavalue":{"value":{"entity-type":"item","numeric-id":24376,"id":"Q24376"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361268$9C084E19-3A32-49AD-9922-5A808330CBB1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"1c1111a4af73946d995c6025450c33305be35b38","datavalue":{"value":{"entity-type":"item","numeric-id":40350,"id":"Q40350"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361268$50A51B93-BBE6-47D7-A3D8-7529E96D169B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"c4aeb66dd27e57f668207276c0a9e7241a80037b","datavalue":{"value":{"entity-type":"item","numeric-id":31438,"id":"Q31438"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361268$99564F17-DA83-482C-80F2-E1A32D9BD5EC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"f63e264dd356e5fd0775265176e22727183a2bbe","datavalue":{"value":{"entity-type":"item","numeric-id":53729,"id":"Q53729"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361268$67FAD2DB-3C05-416E-A335-FF681F015F50","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"6b46a92ecf181aaf6ba95c111143d4a257b6e3e1","datavalue":{"value":{"entity-type":"item","numeric-id":15442,"id":"Q15442"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361268$DA1BF367-265C-4A01-B104-76E818D1FFFC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"ecda3e6d8e971c0b93d4cf3afb41990e853f830f","datavalue":{"value":{"entity-type":"item","numeric-id":13212,"id":"Q13212"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361268$E5961A99-05B4-4A26-A2CB-FAF9FD73AC67","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"1c7dda9137a8c097a2c877519ded8ad19344712a","datavalue":{"value":{"entity-type":"item","numeric-id":31394,"id":"Q31394"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361268$76624B3B-D773-4B1B-868E-3E3F154FAFDE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"7ef1082544496cdbd626aabd0ffce07a1cf4d46a","datavalue":{"value":{"entity-type":"item","numeric-id":40285,"id":"Q40285"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361268$6AB64C05-AFF6-4DA9-B1BC-865B38ECD2C3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"f0874088d59a2cbce379152e0f60bc05817c8d64","datavalue":{"value":{"entity-type":"item","numeric-id":21686,"id":"Q21686"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361268$328E5B16-177C-42F1-9834-40AED63333BA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"2fd4f2f31989858180fba533a04e1a60c8d16377","datavalue":{"value":{"entity-type":"item","numeric-id":22154,"id":"Q22154"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361268$87AEAD2A-8B71-4197-BCB3-CCF643114504","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"95c00ddff627e0bd2ea48a44285988ed2884713b","datavalue":{"value":{"entity-type":"item","numeric-id":20425,"id":"Q20425"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361268$6A25CFE7-9B5D-4251-8FB9-4DA7F8987FB1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"b93a9885014e7b994c6840116d69ecd63fa83844","datavalue":{"value":{"entity-type":"item","numeric-id":19326,"id":"Q19326"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361268$B8CB632D-03AF-4D19-A32A-8C3D814362C8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"cc4eff68b160f30b8d66dfcb610a0ea7a927079b","datavalue":{"value":{"entity-type":"item","numeric-id":17039,"id":"Q17039"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361268$1F7E72A6-2033-4A0F-B2C7-7C4BC75427FC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"8aafdf7df9ab6945d55471b6dee241d20aae57bb","datavalue":{"value":{"entity-type":"item","numeric-id":16290,"id":"Q16290"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361268$3F3CA509-CD3F-40AA-98C0-8C0A878B579A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"1da83e82f563b21e91a419cb34e11d3be154209f","datavalue":{"value":{"entity-type":"item","numeric-id":16295,"id":"Q16295"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361268$238F2899-7CA5-4D2E-93AB-3E384E424628","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Formalization of Bachmair and Ganzinger's Ordered Resolution Prover","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Formalization_of_Bachmair_and_Ganzinger%27s_Ordered_Resolution_Prover"}}}}}