{"entities":{"Q7361845":{"pageid":31521074,"ns":120,"title":"Item:Q7361845","lastrevid":105369875,"modified":"2026-10-07T13:38:39Z","type":"item","id":"Q7361845","labels":{"en":{"language":"en","value":"The Resolution Calculus for First-Order Logic"}},"descriptions":{"en":{"language":"en","value":"AFP entry Resolution_FOL"}},"aliases":{},"claims":{"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"7839a0bfbbfe44cebee4f928f203b685064c7211","datavalue":{"value":"https://isa-afp.org/entries/Resolution_FOL.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q7361845$06D23FCD-42B2-46C0-9A86-4D18158A2DB6","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"7d98f2be9388fe0b19e5e725594ce7a9c36c460b","datavalue":{"value":{"time":"+2016-06-30T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q7361845$DED158E4-0C62-4BC4-9105-E1842CDD9E2A","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"f19e42813e41b1b694ee6662dce0e445e8e41f4b","datavalue":{"value":"Anders Schlichtkrull","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361845$B078C99B-6E70-4B62-BA94-1F787D0E0FAB","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"64a5a49503d0fd265fbb0bdc60369edd09d82f40","datavalue":{"value":{"text":"The Resolution Calculus for First-Order Logic","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q7361845$0075CB60-9033-40A8-9414-C46241EB7D7F","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"902659f760057cf7058e9f886d16cc1aeb6fb3d1","datavalue":{"value":"This theory is a formalization of the resolution calculus for first-order logic. It is proven sound and complete. The soundness proof uses the substitution lemma, which shows a correspondence between substitutions and updates to an environment. The completeness proof uses semantic trees, i.e. trees whose paths are partial Herbrand interpretations. It employs Herbrand's theorem in a formulation which states that an unsatisfiable set of clauses has a finite closed semantic tree. It also uses the lifting lemma which lifts resolution derivation steps from the ground world up to the first-order world. The theory is presented in a paper in the Journal of Automated Reasoning [Sch18] which extends a paper presented at the International Conference on Interactive Theorem Proving [Sch16]. An earlier version was presented in an MSc thesis [Sch15]. The formalization mostly follows textbooks by Ben-Ari [BA12], Chang and Lee [CL73], and Leitsch [Lei97]. The theory is part of the IsaFoL project [IsaFoL]. [Sch18] Anders Schlichtkrull. \"Formalization of the Resolution Calculus for First-Order Logic\". Journal of Automated Reasoning, 2018. [Sch16] Anders Schlichtkrull. \"Formalization of the Resolution Calculus for First-Order Logic\". In: ITP 2016. Vol. 9807. LNCS. Springer, 2016. [Sch15] Anders Schlichtkrull. \"Formalization of Resolution Calculus in Isabelle\" . https://people.compute.dtu.dk/andschl/Thesis.pdf . MSc thesis. Technical University of Denmark, 2015. [BA12] Mordechai Ben-Ari. Mathematical Logic for Computer Science . 3rd. Springer, 2012. [CL73] Chin-Liang Chang and Richard Char-Tung Lee. Symbolic Logic and Mechanical Theorem Proving . 1st. Academic Press, Inc., 1973. [Lei97] Alexander Leitsch. The Resolution Calculus . Texts in theoretical computer science. Springer, 1997. [IsaFoL] IsaFoL authors. IsaFoL: Isabelle Formalization of Logic . https://bitbucket.org/jasmin_blanchette/isafol .","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361845$E74D9BAF-761E-4D39-8FD1-DFF8B2A6E4B0","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"95f5e5a42b14858827b86e355a072cbbd1bdb099","datavalue":{"value":{"entity-type":"item","numeric-id":2894076,"id":"Q2894076"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361845$1A2434A5-55F4-4255-9F88-FC7E28C9B5AC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3a4735154d50c08d584a8e28202802fa9d661654","datavalue":{"value":{"entity-type":"item","numeric-id":5679729,"id":"Q5679729"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361845$D71F0B39-CF99-49EF-82F1-455EFC6396B1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f8755fff25bcbf365d5dd2dfde2f78f833a2371b","datavalue":{"value":{"entity-type":"item","numeric-id":4331764,"id":"Q4331764"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361845$8FA90597-6B88-46E3-9B88-09C54B552500","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"203d48d7253d124888377b269b6bdabd88ab4d55","datavalue":{"value":{"entity-type":"item","numeric-id":2829269,"id":"Q2829269"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361845$C0225F85-E0C8-4FDE-9E0F-A22D1BB4E382","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"38602d2b7fd482d2c85a2b53c450a23a2740fb43","datavalue":{"value":{"entity-type":"item","numeric-id":1663242,"id":"Q1663242"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361845$B0919281-3844-423A-9D5C-88DCB654BF7F","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":"Q7361845$466D9636-BD54-4383-93BA-E27E3C866BF1","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":"Q7361845$E9FEDB20-0957-4D27-8434-E8BF23B7048A","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":"Q7361845$2AD1E525-9B0E-4F99-ADC9-D8531C4A49BD","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":"Q7361845$B82DA6BC-3F49-4442-B988-A592414B3688","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"The Resolution Calculus for First-Order Logic","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/The_Resolution_Calculus_for_First-Order_Logic"}}}}}