{"entities":{"Q1820590":{"pageid":1831332,"ns":120,"title":"Item:Q1820590","lastrevid":77968412,"modified":"2026-05-06T10:28:33Z","type":"item","id":"Q1820590","labels":{"en":{"language":"en","value":"Some remarks on the possibility of extending resolution proof procedures to intuitionistic logic"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 3997189"}},"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":"Q1820590$9B9635F3-9915-4A90-964D-4C188C513A47","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"0116ab7f62ec27e6f5635741c42bf832b2ef3662","datavalue":{"value":{"text":"Some remarks on the possibility of extending resolution proof procedures to intuitionistic logic","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1820590$CD62D216-9A36-48B3-8BA6-47B2142491FE","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"7b557775ebc48c8f1957389bd3c2ecfd28a59b8f","datavalue":{"value":"0615.68060","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1820590$83B76BBF-37CE-4090-9974-6BB758B972D7","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"8b5371afeff2a75d82d453d3fa018ef325128be4","datavalue":{"value":"10.1016/0020-0190(86)90146-8","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1820590$B9DCDB9C-A19C-4778-97BD-E2993E132659","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"52fa7d44b58d0511cb8993765bd916aef86052d8","datavalue":{"value":{"entity-type":"item","numeric-id":63092,"id":"Q63092"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1820590$E81C051D-180F-4F7F-AEE3-4069635B71D8","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"63df7153432d81fa42019fcabb076c89649b0b5b","datavalue":{"value":{"time":"+1986-00-00T00:00:00Z","timezone":0,"before":0,"after":0,"precision":9,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1820590$EAA2BBDF-77EA-45AB-B489-97F296E6C3FE","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"d49a32684845ce5ea8eb45b03e3122aeba1eb653","datavalue":{"value":"The author proposes a resolution procedure for propositional intuitionistic logic, which is indirect: the intuitionistic logic is translated into a modal system to which the rules of resolution are applied. The modal system used (it has the same Kripke interpretation as intuitionistic logic) is the S4 system of Lewis enriched by the axiom: ''p\\(\\to \\square p\\) if p is atomic''. The author defines the modal system, the translation rules, and the resolution rules. Also, a sketch of the completeness proof is presented.    Unfortunately, as the author mentions, the backtrack to intuitionistic logic (possibly limited to this particular approach only) is extremely difficult since, among other things, a modal deduction formula from a set of clauses which translate intuitionistic formulas generates clauses which translate no intuitionistic formula.","type":"string"},"datatype":"string"},"type":"statement","id":"Q1820590$8FF37ABA-840A-4A7C-A431-B60C02EE1CCC","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1820590$576BD5F1-885D-4E14-9EED-F8D0B1015664","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1820590$EED65357-307E-4EC9-9194-0F5011DF9661","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"a0f70162dd8119beb8a7152f993c91e85db34de5","datavalue":{"value":"3997189","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1820590$EB24F4F5-0986-4FD2-B07F-5F14F9D6C591","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a97de3d0557b48460726cb42513fe34c388ae377","datavalue":{"value":"resolution procedure for propositional intuitionistic logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q1820590$EC5BB9E2-E36E-44F8-BDDB-B7720691E2FC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"dac274aaaa1600b9e2193e10311c5a0cb0a67da7","datavalue":{"value":"modal system","type":"string"},"datatype":"string"},"type":"statement","id":"Q1820590$0E86FDA9-3289-48CE-B323-D3E5EC04526A","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"59e85c5db1a6961ef0897daa8abccf0b647303a8","datavalue":{"value":{"entity-type":"item","numeric-id":229749,"id":"Q229749"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1820590$445345E1-136C-4D7D-802F-6C69F3E7F76E","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":"Q1820590$DC4DAB4F-EEE8-4150-A83D-C0B47A7622C7","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"0ed6a4c4f13a6f1d86659a22f1055e7b50b07dad","datavalue":{"value":"https://doi.org/10.1016/0020-0190(86)90146-8","type":"string"},"datatype":"url"},"type":"statement","id":"Q1820590$69EA2B1D-A7A3-48F5-B6FD-12F7B13B6A5E","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"54679af8259210cb29ed65f728e6806bf5d7e391","datavalue":{"value":"W2064239695","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1820590$91473714-1365-4467-B305-AC7DCE8EF201","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"19a962d0a7be8a0ba0ddc1bcd8d1ce60fa548737","datavalue":{"value":{"entity-type":"item","numeric-id":5670174,"id":"Q5670174"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1820590$9111621F-2A15-4A20-B3C9-8E0AEE38E159","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"02be31bbcccdd5668a4bf38db4eb874de330c10d","datavalue":{"value":{"entity-type":"item","numeric-id":1051424,"id":"Q1051424"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1820590$81433ECB-9F72-4C55-9DA8-C9ADB4FB962D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c975ae90a4763199c30a8e67e2f030e9206a8178","datavalue":{"value":{"entity-type":"item","numeric-id":1051628,"id":"Q1051628"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1820590$7E45A5BA-5B33-49DF-9345-707D001FF751","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1435f3ecb80e66ef3a6c0e0b3b5e54cc7cafb970","datavalue":{"value":{"entity-type":"item","numeric-id":3880322,"id":"Q3880322"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1820590$1C5CFCEF-D782-47EA-928A-41F700FCF3A7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b19af37d190007ff6ebc0d93b6c1957931f3dcf9","datavalue":{"value":{"entity-type":"item","numeric-id":4698331,"id":"Q4698331"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1820590$86D4F7BF-C78C-4920-AF69-7365DE6B50EE","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":"Q1820590$213F40B2-3319-444B-B10C-B0F178BF55C5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"dd7f4ac2c4d2314fae83403dbcb7eab5f78434cd","datavalue":{"value":{"entity-type":"item","numeric-id":3864488,"id":"Q3864488"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1820590$58E0A3DB-CB2C-4C36-8B9B-B3C0A7D9B909","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"93c080708c3bbeeffbe569dfaf09fc9efb27ce99","datavalue":{"value":{"entity-type":"item","numeric-id":4312461,"id":"Q4312461"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0e3f46cacf6d2ee8055338a15067a375b89ccf9b","datavalue":{"value":{"amount":"+0.8377689123153687","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":"Q1820590$3D99EE05-0343-4791-A37F-30611047E8E8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"92939b86137af1b0455e2845a510c8f884a99fbc","datavalue":{"value":{"entity-type":"item","numeric-id":1178699,"id":"Q1178699"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"092b21ef769011aa589c98a1c991506871c463a6","datavalue":{"value":{"amount":"+0.8281705975532532","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":"Q1820590$C5039DD8-555E-4233-8E7D-D669F81534B1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2bc88718a305d147397faaf7899d51ccdc2bb5ca","datavalue":{"value":{"entity-type":"item","numeric-id":4647496,"id":"Q4647496"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1ec53dfdba31a60db21faa9009c64ce05316a334","datavalue":{"value":{"amount":"+0.8195960521697998","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":"Q1820590$1492CFC6-A8F9-4793-B1CE-7B71960CE4CD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7bfd9cacfb382743e4e8b8fba5485149f15e1ab4","datavalue":{"value":{"entity-type":"item","numeric-id":3768867,"id":"Q3768867"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7a9861bd9424f2fc25e51da68aa1fd7d7593dc49","datavalue":{"value":{"amount":"+0.8128620982170105","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":"Q1820590$601A7F35-983A-4193-BABA-950B37E587CC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"af54e2880b1d9f1bb1a6f99406e59c4bdc2b79dc","datavalue":{"value":{"entity-type":"item","numeric-id":3211281,"id":"Q3211281"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"49432ba2a680d662fa636ca9c4f3710eac773763","datavalue":{"value":{"amount":"+0.80495285987854","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":"Q1820590$6082FC53-1FFE-4348-82F8-FC396B7766CA","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Some remarks on the possibility of extending resolution proof procedures to intuitionistic logic","badges":[]}}}}}