{"entities":{"Q685363":{"pageid":687212,"ns":120,"title":"Item:Q685363","lastrevid":63459564,"modified":"2026-04-11T13:18:14Z","type":"item","id":"Q685363","labels":{"en":{"language":"en","value":"On generalized Horn formulas and \\(k\\)-resolution"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 417321"}},"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":"Q685363$34D9488D-2EF5-41B6-B88B-9E5C08BE6AF5","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"4448cc1fa80bd2286f7a07152d8464e692d523b6","datavalue":{"value":{"text":"On generalized Horn formulas and \\(k\\)-resolution","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q685363$AD39D3A8-9E0B-4A3F-A836-BA4ECDD87A96","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"b9d704ca0be375607a529b9e92070e2d0c7f45c9","datavalue":{"value":"0786.03009","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q685363$7246640D-52D0-4624-BCA0-E049225EE25F","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"6dd0d08f7f06c73f148fdd2eef290f54d44c7b13","datavalue":{"value":"10.1016/0304-3975(93)90331-M","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q685363$C90FC332-7086-49FB-90D1-591A40492B7E","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"9fa6eeb09e47d0c3657c971f131f2ff7452bd83e","datavalue":{"value":{"entity-type":"item","numeric-id":599500,"id":"Q599500"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q685363$60D44474-7FF0-4F96-B97A-F086B454A9DB","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"f3c424cd94a60f9664f9fb69cc6027e75cc7ff3f","datavalue":{"value":{"entity-type":"item","numeric-id":123643,"id":"Q123643"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q685363$ACBA4AAC-37B0-4DB2-AB7C-1E7772BECF68","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"ae4d7b05535bc7692a75fc587d4810a7bdebded5","datavalue":{"value":{"time":"+1994-05-05T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q685363$FB550CC2-CB53-4927-9CF5-2157F7FEFDA3","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"a01d7c1f2dc1eaae2537a68583e1c367c5c508c9","datavalue":{"value":"Several approaches to extend the set of Horn formulas to classes of CNF formulas for which SAT problem is still polynomially solvable have already been made. The paper presents a series of results concerning the satisfiability problem for the classes of propositional formulas belonging to the hierarchy introduced by Gallo and Scutella in 1988. The satisfiability problem for the class of \\(k\\)-generalized Horn formulas \\(H_ k\\) is treated in the framework of bounded-unit preference strategy based on an appropriate generalization of the resolution principle referred here as \\(k\\)-resolution. The completeness and soundness property of \\(k\\)-resolution for the class \\(H_ k\\) is proved first (theorem 3.3). Next, in theorem 3.5, the author establishes the insufficiency of \\((k- 1)\\)-resolution in deciding the satisfiability for \\(H_ k\\). It is pointed out that, in general, it is necessary to apply the \\((k+1)\\)-resolution to obtain all derivable literals. In the final section of the paper some comments concerning LLRI and 2-resolution are formulated. It is proved that any LLRI-refutable formula is 2-refutable too, but 2-resolution is strictly more powerful than LLRI.","type":"string"},"datatype":"string"},"type":"statement","id":"Q685363$24D215F9-6520-452A-BA11-CF0A1770D6A9","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q685363$58D903C0-59F1-4A90-97E1-7929F9631DBB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q685363$88F3093C-54A7-42E0-B09B-B16D942B4547","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"62ae2f4e9717dc72a20d2c4f17bdde30d85a417c","datavalue":{"value":"68T27","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q685363$98FEE4E4-1BD0-423D-B754-FF21D577AE55","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"d971f250f4b60bd91da7e9350568180af141e6af","datavalue":{"value":"03F03","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q685363$F96D73C1-F01B-4DD5-9EB1-5EFA05B28AAE","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"abb74d9d5a89fa95cebd890d394446a5601c9b2a","datavalue":{"value":"417321","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q685363$56A6A91C-6C70-46D1-AA8D-E836517D5813","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c6c78685aea0a7d91e6d41499c27d1163c6afe98","datavalue":{"value":"refutation","type":"string"},"datatype":"string"},"type":"statement","id":"Q685363$3226EE2E-A209-41CB-A0A6-254808B71E24","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"2ef3d1e723a50ff6e761b841dc7be35b8a1ffc8a","datavalue":{"value":"Horn formulas","type":"string"},"datatype":"string"},"type":"statement","id":"Q685363$2EBA6EE2-FFDA-4722-B28D-4207CDCB7FB7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"252f9f9ed9fe8ca406cc19fba38a46c0414791ee","datavalue":{"value":"satisfiability","type":"string"},"datatype":"string"},"type":"statement","id":"Q685363$51756478-C300-46A7-BD43-7C338BCFC2EE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"cfac5eb6431ec88e2a6e9bafbfcf7b49dda794fc","datavalue":{"value":"resolution","type":"string"},"datatype":"string"},"type":"statement","id":"Q685363$ABF5B888-5145-48F7-838A-0D4D9CB023C5","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"00dcf12b9a602d9c5eb5566a233851af0f0ed4fd","datavalue":{"value":{"entity-type":"item","numeric-id":469832,"id":"Q469832"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q685363$E13F951F-C360-4AF1-910F-1758BB79C0CE","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":"Q685363$2CFDC9E1-F558-43D1-80B3-309314D9D204","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"b3c464582ae733c7e854270d41591b96fb4b962f","datavalue":{"value":{"entity-type":"item","numeric-id":1097717,"id":"Q1097717"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q685363$050210C8-D91A-4370-BD76-F9A66797D3BC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d6b5b0535e606fd0713aa3bc3ecec575e7f5e28b","datavalue":{"value":{"entity-type":"item","numeric-id":3898029,"id":"Q3898029"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q685363$4C4E1630-ACEB-47F5-8450-F2F4B71EBEA0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"84e0ec301a2daa50bbddaee495d81db74f852f2b","datavalue":{"value":{"entity-type":"item","numeric-id":5613968,"id":"Q5613968"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q685363$E423AB26-961A-4B5F-8441-8B0A1A1CFC74","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0a73f079fad88596351ff709cf186cec234a2805","datavalue":{"value":{"entity-type":"item","numeric-id":3723723,"id":"Q3723723"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q685363$40607EBA-4EA3-4576-A65F-1117C4481902","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"51ecb7524e03e885eff0a1c3c3b63046bd70d1cd","datavalue":{"value":{"entity-type":"item","numeric-id":1114394,"id":"Q1114394"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q685363$F94D916D-F053-40DE-928D-7D4A9BF03A96","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3b353bc1298597265c71a16d3c350d4e62f0e57f","datavalue":{"value":{"entity-type":"item","numeric-id":3677734,"id":"Q3677734"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q685363$FA196CA8-F1BC-4E8A-8EC2-03CCE7BED59F","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"98a5d2019855f6cb988265a2308dc94067de4907","datavalue":{"value":"https://doi.org/10.1016/0304-3975(93)90331-m","type":"string"},"datatype":"url"},"type":"statement","id":"Q685363$0DE0CC61-9EF6-489E-A6E2-26FA2894CBFD","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"698b77103f7e39796a0325e64c4a8ee314c04831","datavalue":{"value":"W1504884225","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q685363$8889A1F7-5995-4C93-A68F-E95B4B2322A3","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6998c936108abd7bd709a773ce14ea6acbfea98a","datavalue":{"value":{"entity-type":"item","numeric-id":1380411,"id":"Q1380411"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"149a0c2b69b03e0ad93e6062c2153898f213b6b4","datavalue":{"value":{"amount":"+0.795616090297699","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":"Q685363$3A477929-175E-465E-87FA-42856A3C1B32","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9dff7bcce7cc9619d1f2879285177956c39aab73","datavalue":{"value":{"entity-type":"item","numeric-id":2387427,"id":"Q2387427"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"13b2db237f00baf9b1896fb2bd7fefc9e2e59d32","datavalue":{"value":{"amount":"+0.7832094430923462","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":"Q685363$2D9ED7D9-F549-4527-9AE5-F3E837C0CDDF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9c48f56e941190cd2911d5ff958db66c22ca9b5c","datavalue":{"value":{"entity-type":"item","numeric-id":1114394,"id":"Q1114394"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ce2bb50a6be09aafcad1a6f6cd7396d718b36e0e","datavalue":{"value":{"amount":"+0.7702370285987854","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":"Q685363$272C169E-5531-447F-9FDD-B7F72CD60133","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"04415b4acfa317c05592d9e4057f2a56b8a072ef","datavalue":{"value":{"entity-type":"item","numeric-id":3815282,"id":"Q3815282"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7e04a1e4823235d61bdf835283b0757e2ca84d2f","datavalue":{"value":{"amount":"+0.7645272016525269","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":"Q685363$7561A449-CF9D-4C77-A6FA-39A6E667E09E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e62c79a068b58ae88207b93c2f4c580ac15af758","datavalue":{"value":{"entity-type":"item","numeric-id":3006475,"id":"Q3006475"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2364773e896f939a5064db87d5f43c8e3f9d307d","datavalue":{"value":{"amount":"+0.7624822854995728","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":"Q685363$6B63B0B8-F993-4ED7-B52C-8D8BD67FBB51","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"On generalized Horn formulas and \\(k\\)-resolution","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/On_generalized_Horn_formulas_and_%5C(k%5C)-resolution"}}}}}