{"entities":{"Q53728":{"pageid":53784,"ns":120,"title":"Item:Q53728","lastrevid":105428873,"modified":"2026-10-09T10:10:47Z","type":"item","id":"Q53728","labels":{"en":{"language":"en","value":"Ordered_Resolution_Prover"}},"descriptions":{"en":{"language":"en","value":"AFP entry Ordered_Resolution_Prover"}},"aliases":{},"claims":{"P13":[{"mainsnak":{"snaktype":"value","property":"P13","hash":"0c1cc967e825a90ea00b878af0be1c66d00e5062","datavalue":{"value":"38028","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q53728$896A2E48-B7B2-441D-BCB2-79FE6DB7F186","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":"Q53728$728E7791-7FE7-410A-8DCA-5B20ECD9AE15","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":"Q53728$6B377BCD-88C2-4811-888C-B02949B1FA42","rank":"normal"}],"P29":[{"mainsnak":{"snaktype":"value","property":"P29","hash":"7c4014c3313a8b16bf58ce24eebb76e1f7689e88","datavalue":{"value":"https://www.isa-afp.org/entries/Ordered_Resolution_Prover.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q53728$ECE26781-98E1-4BE0-8D74-1DD270D30EC0","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"0db99c3b17fc587dc6d0b047e5ff5ce0de1786ab","datavalue":{"value":"03","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q53728$029EC42E-FC3A-4445-830D-F5EA535C95A2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"acf10290b955a69659a681d98822944f91bbad9e","datavalue":{"value":"68","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q53728$5D5FA020-D111-414A-8CED-81101F85F028","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"9ccfc2ffdb7a60cd36d8dca0a4e6d9d45f5228f3","datavalue":{"value":"3","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q53728$F2F4B4B9-4351-4F6B-B684-CA748812ADEC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"09f5e0c6033338f59ef27e37d6877da0f26d9646","datavalue":{"value":"68.0","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q53728$0DC6512C-E247-4138-A658-6F3A32CBFE47","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":"Q53728$DD90219F-EF6B-4FF0-9780-5E0BEA8481D9","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":"Q53728$B027D59D-40C8-4CCB-AF21-A823A0BAFE97","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":"Q53728$4E2D2418-8788-489B-B1FA-2DB66217D4D5","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":"Q53728$91D46FD0-68F6-472C-A462-661CD1781E09","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":"Q53728$6E0C6C44-F69E-4E7A-8E17-952FB394B874","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":"Q53728$BD7A5C4A-E219-43DC-A6B7-44F7A899381D","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":"Q53728$30235469-8C3D-4418-A9B3-DFC588FB8DBB","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":"Q53728$6568F6F5-2F31-448B-AC68-74D99EF175D1","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":"Q53728$2847ACBE-0F5C-408E-BB57-2C92E607E09F","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":"Q53728$66E2435D-7E03-43A3-87B2-CAE5B6E003E2","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":"Q53728$9B70A148-12EF-4AAF-9366-A909CF4A0642","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":"Q53728$907064AD-424F-4643-9BD5-8FAC12007867","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":"Q53728$F0D67E76-FA1B-485A-9215-5B491B404C5C","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":"Q53728$F6D57D30-197D-4B3F-AA29-79640274DECD","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":"Q53728$12112B8E-F972-4C00-ABC4-71479CDBF3D6","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":"Q53728$10E061E5-C8EF-4331-95F1-A866247FA4EA","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":"Q53728$92D69313-549E-496D-9C74-CF0133EA8315","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":"Q53728$80277C23-D2CA-4458-918E-1F2CCD3AAD6A","rank":"normal"}],"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":"Q53728$FA406AB5-DD27-4FFC-924F-23B06B2A5072","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"f19e42813e41b1b694ee6662dce0e445e8e41f4b","datavalue":{"value":"Anders Schlichtkrull","type":"string"},"datatype":"string"},"type":"statement","id":"Q53728$33BB1717-E62A-45D9-A3DF-B271A4F12789","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"d593b6f197721b1ecf9f17d8e5bbb2bb5a1f7f8a","datavalue":{"value":"Jasmin Christian Blanchette","type":"string"},"datatype":"string"},"type":"statement","id":"Q53728$76E453CD-C1E4-42B5-A137-0F286FE35E99","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"2500aa80beaafa12dfa4ab6c7d8363674f762e6e","datavalue":{"value":"Dmitriy Traytel","type":"string"},"datatype":"string"},"type":"statement","id":"Q53728$43BC5AAE-D51E-4CAD-9639-D5A0D0E72A5A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"0bea28856612bb879f597a9d9f573ece274a0783","datavalue":{"value":"Uwe Waldmann","type":"string"},"datatype":"string"},"type":"statement","id":"Q53728$F070999F-BE3B-4A2D-B0F5-D894A00A2047","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":"Q53728$557E857B-5C52-4AB2-A305-B0D07E4DF45E","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":"Q53728$AB32D232-917B-4139-B2EF-4F5037964C26","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":"Q53728$B47CC112-E32D-4D6C-80E6-75F92497DD5B","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":"Q53728$CD2B6712-E8F9-47DB-8DC3-3B13FCC837AE","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":"Q53728$DECD0AD0-01C0-4471-88F7-5AA313A1D383","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":"Q53728$27D2927E-8852-4A6C-8F25-F0A802F02369","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":"Q53728$CB68885B-2E41-4BC6-BC15-36468493E844","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Ordered Resolution Prover","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Ordered_Resolution_Prover"}}}}}