{"entities":{"Q636273":{"pageid":638121,"ns":120,"title":"Item:Q636273","lastrevid":63302646,"modified":"2026-04-11T11:57:55Z","type":"item","id":"Q636273","labels":{"en":{"language":"en","value":"Extracting the resolution algorithm from a completeness proof for the propositional calculus"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5943593"}},"aliases":{},"claims":{"P31":[{"mainsnak":{"snaktype":"value","property":"P31","hash":"fd5912e4dab4b881a8eb0eb27e7893fef55176ad","datavalue":{"value":{"entity-type":"item","numeric-id":56887,"id":"Q56887"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q636273$286E49FD-21DF-498B-8071-6F4F1C99293A","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"1351deba65e4371a2380e77e0cadbcd2e3f99e36","datavalue":{"value":{"text":"Extracting the resolution algorithm from a completeness proof for the propositional calculus","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q636273$733F9B82-FC52-4193-930A-2FB74783BD57","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"020f2991fd0fe30f01e7a42cbb1eba89a77bafcb","datavalue":{"value":"1221.03015","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q636273$F50F97CA-7531-423D-81F3-7A528CB02119","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"e7d45bc58b6343c85796331c2c0125934a8b7086","datavalue":{"value":{"entity-type":"item","numeric-id":408533,"id":"Q408533"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q636273$038677C4-E9DF-4603-AC96-7E09E04E15BE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"c9f99e72dec046038a5377ceee67d8841bab629f","datavalue":{"value":{"entity-type":"item","numeric-id":1051423,"id":"Q1051423"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q636273$9AA8D419-12E8-4932-AF85-3677EECD6D93","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"f91a4bcbc93435aed71775d25a4c5cd09e26f12d","datavalue":{"value":{"entity-type":"item","numeric-id":122505,"id":"Q122505"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q636273$A08D145D-CAB4-4F8D-A871-40E04CDC16B9","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"b8f347fb3b92d10259e32e7ae3b68d43ebb98729","datavalue":{"value":{"time":"+2011-08-26T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q636273$A12AAD37-9C0A-45E5-A387-FC505DC033EA","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"f646b82507ac918081383a644f49b6c0086e21a1","datavalue":{"value":"https://hdl.handle.net/1813/5754","type":"string"},"datatype":"url"},"type":"statement","id":"Q636273$62629DDC-2D7E-4F70-8B3B-1D854152C45D","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q636273$FE455460-2FA3-48CC-8584-409B93563D17","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"419d6f2b09c39920e34f63114ff159a2f0a01812","datavalue":{"value":"03B05","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q636273$D4C2B71C-3344-4A8B-9D25-5FD906D8924A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q636273$2C55B42D-76BF-4449-993C-6E22146561B3","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"f413ad32bb7f5c3c2049792de2dfd5dc0960a60b","datavalue":{"value":"5943593","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q636273$674E86BA-10FA-4EFC-8F39-8884F47B2C2B","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5ea0e35eece84bed33461e424b92d07e45bd0c24","datavalue":{"value":"type theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q636273$97674856-8F7C-430E-9695-494F83CFA2A0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"cfac5eb6431ec88e2a6e9bafbfcf7b49dda794fc","datavalue":{"value":"resolution","type":"string"},"datatype":"string"},"type":"statement","id":"Q636273$C649E3D8-2D56-4149-935E-47D75CE7C4CD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"36a96860261afab88486624af0939a44f9aa584f","datavalue":{"value":"program extraction","type":"string"},"datatype":"string"},"type":"statement","id":"Q636273$66B98321-4F55-4431-B5AA-3B1AA5C47306","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1ca1042868ff4f694776e4b2c62ec66638c4ef91","datavalue":{"value":"automated reasoning","type":"string"},"datatype":"string"},"type":"statement","id":"Q636273$140D120F-E8C5-478C-A162-450A54A75305","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a7a416e0b794520b49bf582a85e2ef29f146f045","datavalue":{"value":"intuitionism","type":"string"},"datatype":"string"},"type":"statement","id":"Q636273$B16CD748-7F76-4E9F-9C1E-947F9947B585","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"09e5b68927baf737cf4d5adadb4664c931aae1c2","datavalue":{"value":"Coq","type":"string"},"datatype":"string"},"type":"statement","id":"Q636273$9BAC8575-C070-4D69-BA06-13BC0541F307","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"846a4e298fc723066f7d4f0359d577bc33c21605","datavalue":{"value":"Haskell program","type":"string"},"datatype":"string"},"type":"statement","id":"Q636273$407FC05C-E0F0-4547-8096-038139AAEA57","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"70c51cb69cf83ba52d30c7a2c9abf4fc48a6f8a5","datavalue":{"value":{"entity-type":"item","numeric-id":18707,"id":"Q18707"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q636273$0C6B1107-437F-4811-A224-49C10F893FCC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ab6ee58efeeaa685ac2b8ecf828badcfb673e8c7","datavalue":{"value":{"entity-type":"item","numeric-id":12929,"id":"Q12929"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q636273$97E2E434-802A-4225-8C4C-6DEA573AE100","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"067e00213990a6f2431e78667be3f10443c92f4f","datavalue":{"value":{"entity-type":"item","numeric-id":16052,"id":"Q16052"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q636273$80EF020B-7E4F-4C6F-94A4-5C243D5EE475","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"27b6ae20da44d6f09b655d9481cc0df08a8ffcdf","datavalue":{"value":{"entity-type":"item","numeric-id":18826,"id":"Q18826"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q636273$309EAF7E-9AD3-4482-A223-E8BEBA82D1F5","rank":"normal"}],"P1460":[{"mainsnak":{"snaktype":"value","property":"P1460","hash":"57f7fea50d2ce1b39b695c4a1313582eed405e38","datavalue":{"value":{"entity-type":"item","numeric-id":5976449,"id":"Q5976449"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q636273$5CBDEF86-DAAA-485A-9669-F332FE567CC4","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"5a85d81c93642e2711fbed9436241843570e5031","datavalue":{"value":"W2022840750","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q636273$4FC8CD25-1758-4AD6-852A-F071F32670EE","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"bbd46e00e025849b54a0892b5e385ef0d563478f","datavalue":{"value":{"entity-type":"item","numeric-id":1393228,"id":"Q1393228"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q636273$E8A8D24F-098F-4394-9811-D3D3767D0250","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e9fa3961aef1231c96f05295929316b4bf9d63df","datavalue":{"value":{"entity-type":"item","numeric-id":3484381,"id":"Q3484381"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q636273$7497FB59-F2B8-4A1F-8FC9-55199A1F2797","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9595474d6c649f08e5d55140eff822a5539301af","datavalue":{"value":{"entity-type":"item","numeric-id":3613407,"id":"Q3613407"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q636273$1F1F91D6-7430-42DE-8189-B74496443851","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b8bf1eb0085816c68ff7078182501fe6b0337105","datavalue":{"value":{"entity-type":"item","numeric-id":3743300,"id":"Q3743300"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q636273$14A96E6A-6779-4F09-9A3C-1601E1BFAAA4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"22af49b64da5778569501b563fe96f98a9f44d8d","datavalue":{"value":{"entity-type":"item","numeric-id":5310674,"id":"Q5310674"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q636273$2C76266B-477A-4AFD-A29A-695A7A3E8A54","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f62ebef9379ad97d2bdc3c2e7f5717f221d056cb","datavalue":{"value":{"entity-type":"item","numeric-id":5514129,"id":"Q5514129"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q636273$F7C9ABE9-51DF-478F-86D3-5E585B1A33A0","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"7de65eb54f4c87f832a0c20ed1b239e96f6725a7","datavalue":{"value":"10.1016/J.APAL.2009.07.008","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q636273$E4B2B059-B08F-4321-8F6E-ACF695F60C79","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4821d184ef83e5752c967d173acfc4a04c2e4cff","datavalue":{"value":{"entity-type":"item","numeric-id":5434504,"id":"Q5434504"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4d2a25a55b195899b78faa977abde378b636232f","datavalue":{"value":{"amount":"+0.997900366783142","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q636273$EBDB9630-6070-48C2-860B-11309863953B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4cf7b2dee4bced2cbc9a4883c47f4dd252915b35","datavalue":{"value":{"entity-type":"item","numeric-id":5310674,"id":"Q5310674"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0ccb0828755fa3d56458eb59696999b32ddf58cc","datavalue":{"value":{"amount":"+0.8285399675369263","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q636273$B2C40CBF-EDBE-48C9-B2BB-E13C2B4AACAD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"124bff4b11e7066a44bdfd98c630a15a312c2c3d","datavalue":{"value":{"entity-type":"item","numeric-id":5177337,"id":"Q5177337"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"35774bc55f853dceffd096d75c8081b939890292","datavalue":{"value":{"amount":"+0.7987407445907593","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q636273$367574DF-52D8-4341-8171-C3EC1ABE010F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"45d4a06ef86ca1f117df35c39655a16ae19e64e6","datavalue":{"value":{"entity-type":"item","numeric-id":3178287,"id":"Q3178287"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ea2e51027d0ea3083dbc1b22dbf0b520daa5448a","datavalue":{"value":{"amount":"+0.7980825304985046","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q636273$E44A23FC-7F0E-4762-9733-88CEC2AE49F7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"28a288adf15a2c7507bec1f91484682a9302bbc5","datavalue":{"value":{"entity-type":"item","numeric-id":4847378,"id":"Q4847378"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4b7551607f1543db677e538b168068c59e4d8b4c","datavalue":{"value":{"amount":"+0.7455450892448425","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q636273$EE002CE4-A578-4EF8-9A98-69C474157383","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Extracting the resolution algorithm from a completeness proof for the propositional calculus","badges":[]}}}}}