{"entities":{"Q1819946":{"pageid":1830688,"ns":120,"title":"Item:Q1819946","lastrevid":69402450,"modified":"2026-04-13T06:45:52Z","type":"item","id":"Q1819946","labels":{"en":{"language":"en","value":"Resolution deduction to detect satisfiability for another class including non-Horn sentences in propositional logic"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 3995081"}},"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":"Q1819946$0A46A229-A637-4DDF-9820-8DA4A1AE16C9","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"56ccaa2ee475d68af7671a08b5481d1ae5761d9a","datavalue":{"value":{"text":"Resolution deduction to detect satisfiability for another class including non-Horn sentences in propositional logic","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1819946$8E65DDBE-37D2-46F4-A5DA-2288A9725F50","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"400a8495789f7874147c7e48b76fea4d41ffe76f","datavalue":{"value":"0614.68063","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1819946$62882A7D-2E2D-484C-8718-4ECF22477DBE","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"33c9012d551e1371ac58a0840c85f06d5db1d648","datavalue":{"value":"10.1016/0020-0190(86)90136-5","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1819946$67792B5F-EB67-4B45-ADCB-8027D9A8A6F2","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"514c693109916bc609b6d9a8d6e9cb7af13094b6","datavalue":{"value":{"entity-type":"item","numeric-id":920623,"id":"Q920623"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1819946$B2F139E1-3937-4188-8462-87ED5074278A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"00bde3ded8f72a5c0d13fc0a4948f2385b8ecaf2","datavalue":{"value":{"entity-type":"item","numeric-id":685127,"id":"Q685127"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1819946$A6F469B5-4273-4E85-9610-E9235A969404","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":"Q1819946$C03D19B0-B579-4CEE-AE51-92399D513BD6","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":"Q1819946$1D0D4E91-D745-4D98-8536-7EADEF058690","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"c03f1cddfb5210596f34bae6d5af92bfa17db67d","datavalue":{"value":"The computational complexity of the propositional Horn-clause logic is significant, since its satisfiability is decidable in polynomial time, although the satisfiability problem of the propositional logic is NP- complete.    From the standpoint of NP-completeness, there have been many attempts to extend as much as possible the class of propositional formulae for which the satisfiability problem is in P. This paper is thought of as such an attempt. We propose a class of non-Horn sentences, for which the satisfiability problem is in P. To detect the satisfiability for such a class, we treat an extended version of linear layered resolution deduction based on input deductions, which is formed by repetitions of input deductions with derived unit clauses to be memorized.","type":"string"},"datatype":"string"},"type":"statement","id":"Q1819946$BAA69E30-4A64-4E07-AFAC-927A1BDF4080","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1819946$12BE8CC6-EE64-45CE-B340-610A3BF44EC5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"fdd9498216d1fd2eff80e5a7d18782b649eb7b2f","datavalue":{"value":"68Q25","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1819946$49512889-871F-4194-ACB8-0F850B9CA5D4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"b8e3f40e3cc87753c4e0b7d7ce4bdc00805f626f","datavalue":{"value":"68N01","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1819946$03690EDD-11D9-4855-B1A0-24147E9771F0","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"ac102fa2c26d3e7b8ad23351894a43dcc9743108","datavalue":{"value":"3995081","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1819946$46BDE798-9E92-44CB-9E62-2203E3B5F50C","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"2ba0cc3f7aaac8445724ef309c9eecb57f5a563d","datavalue":{"value":"computational complexity","type":"string"},"datatype":"string"},"type":"statement","id":"Q1819946$48716EAA-F9A0-4264-BC45-216AD107E231","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"97c799f98d5b8ec03ce8786ede25e3ffc0fa1b7e","datavalue":{"value":"propositional Horn-clause logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q1819946$301C88AD-B416-4D19-96D7-6B37671FE3A1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f0b4d6e6089943a261128dec792d30fd4cdc9763","datavalue":{"value":"satisfiability problem","type":"string"},"datatype":"string"},"type":"statement","id":"Q1819946$924B4FEB-B4AA-4DB2-8890-14911B27644A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"cf1bbad404b660dcc4f7e1f74269a25b269f6b2f","datavalue":{"value":"NP-completeness","type":"string"},"datatype":"string"},"type":"statement","id":"Q1819946$C3DDA6A6-CD74-45BF-BB93-52AB193AE1A9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d1a6eca3f6f22c9baa2e2b135d12f50191dceedc","datavalue":{"value":"non-Horn sentences","type":"string"},"datatype":"string"},"type":"statement","id":"Q1819946$81ABDC60-057E-47F9-8E86-6CBE1953175E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"02c8b325a347d40df2aa9442f994d9007b17ede8","datavalue":{"value":"linear layered resolution deduction","type":"string"},"datatype":"string"},"type":"statement","id":"Q1819946$DC7DB8BB-A059-4AB0-B712-AC83E36A504A","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":"Q1819946$38F4BF98-440A-4FB1-B26F-5DB639DB10ED","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"ea2a7686f5a1558f46915770346e1ab0ddd1e26f","datavalue":{"value":"https://doi.org/10.1016/0020-0190(86)90136-5","type":"string"},"datatype":"url"},"type":"statement","id":"Q1819946$72FB04E9-2EA0-4F75-BEF0-0A6A2180A0FD","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"a7502d1a6ed6b47385afee5a1d06683ff185a903","datavalue":{"value":"W1986931182","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1819946$A4E88D5F-1856-41EE-B494-9292F50829A1","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"dd3a7cfeece8562a9ac87120b107e2b528967937","datavalue":{"value":{"entity-type":"item","numeric-id":4773298,"id":"Q4773298"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1819946$4E61C0C1-9285-491A-90D9-0C2C6F6F3BF9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"08b8154126bb7dcff376a3fb5230eefc60388d66","datavalue":{"value":{"entity-type":"item","numeric-id":5652222,"id":"Q5652222"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1819946$2052446E-90ED-44B3-8058-9C307C2FE2DA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ef757ecac8e00102e8fe2d81d7657ee3391ff698","datavalue":{"value":{"entity-type":"item","numeric-id":4138187,"id":"Q4138187"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1819946$7BCAB2AA-9E87-4C32-832C-7D862781D434","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a35cc55e5b10a424a85f3ddcd5c540cf5328ff0d","datavalue":{"value":{"entity-type":"item","numeric-id":1249435,"id":"Q1249435"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1819946$F725B8E6-6B45-439B-A578-BB8855FC6E55","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"836ad2a04f82225da478ca9f694f5cd99360b315","datavalue":{"value":{"entity-type":"item","numeric-id":4198056,"id":"Q4198056"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1819946$0AFA83E9-4797-4914-B5D4-588B4EE016CC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"041184ced68ec1bcfc7e3558db4714d4dc908858","datavalue":{"value":{"entity-type":"item","numeric-id":4050192,"id":"Q4050192"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1819946$C6F209E2-6886-4318-B185-640B9652E6DE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"373c65ef4069b52a23fe230e08a271e32f56a00a","datavalue":{"value":{"entity-type":"item","numeric-id":1235982,"id":"Q1235982"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1819946$F75BB43E-E5D5-49E9-924E-C8D05095BA50","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"dda6d4bc4ff06358c5dfe216b9a7a58bec1514be","datavalue":{"value":{"entity-type":"item","numeric-id":4102765,"id":"Q4102765"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1819946$31790D43-7EFE-4CC0-8E24-60F80252253E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"755b705d434743289f1c33d94607b3327759f7e3","datavalue":{"value":{"entity-type":"item","numeric-id":4142699,"id":"Q4142699"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1819946$26016BB0-E09B-4696-99BC-E1F8FD2A1452","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8c8a79af3c28ca6a85273f2cf60e4233483e6da8","datavalue":{"value":{"entity-type":"item","numeric-id":4051550,"id":"Q4051550"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1819946$8FAD831D-705A-4884-A90D-EF5D24B61D73","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7f4bcd76765332f83ca0d4b037c13ff8aba19c47","datavalue":{"value":{"entity-type":"item","numeric-id":4132514,"id":"Q4132514"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1819946$C93CE63F-1DC6-477B-B49D-7D7953C48BD7","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a27e17451f20c33485f58a57d2667b7321d08684","datavalue":{"value":{"entity-type":"item","numeric-id":3677734,"id":"Q3677734"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e81c7f8d942d8940f9a8cb977fd1fb9e87d95d84","datavalue":{"value":{"amount":"+0.8326669335365295","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":"Q1819946$8EFBDAB7-963A-4A79-B6C0-323ADDD66B5D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"510b265ea165e0d6552a3dd321cab1d3b9a34f43","datavalue":{"value":{"entity-type":"item","numeric-id":4315881,"id":"Q4315881"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"985c40d4fa2ff18d918630fd31a1f52d029f9f09","datavalue":{"value":{"amount":"+0.7857825756072998","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":"Q1819946$69E67653-D831-42D2-9118-49355AFCE5DB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b7e7e169433d0369f37f847f1d0ec7a8a26bcb86","datavalue":{"value":{"entity-type":"item","numeric-id":1329742,"id":"Q1329742"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"06874f91c57ac9786ab0dc478e5e8f9f6e9fbb77","datavalue":{"value":{"amount":"+0.7852713465690613","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":"Q1819946$A81ECAB3-1007-4054-93A9-BCE5C8899919","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6b4df11fc868397d19521e862b6fa5bae8dba047","datavalue":{"value":{"entity-type":"item","numeric-id":1097717,"id":"Q1097717"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"42deb007fddd20e9bb24afe6dbad0180b720bf97","datavalue":{"value":{"amount":"+0.7848672866821289","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":"Q1819946$185D3AE6-7C1B-4A25-A3C9-26E344CC6449","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d1b3677be470c48f9f6b1444f1d190a74f1739f2","datavalue":{"value":{"entity-type":"item","numeric-id":4488342,"id":"Q4488342"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e6904fc8c2def39a736cadd92fbb11dcfe448c4a","datavalue":{"value":{"amount":"+0.7789491415023804","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":"Q1819946$E3945423-D179-40D5-A7F9-F788689F5819","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Resolution deduction to detect satisfiability for another class including non-Horn sentences in propositional logic","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Resolution_deduction_to_detect_satisfiability_for_another_class_including_non-Horn_sentences_in_propositional_logic"}}}}}