Read-once resolutions in Horn formulas. (English) Zbl 1525.68196
Chen, Yijia (ed.) et al., Frontiers in algorithmics. 13th international workshop, FAW 2019, Sanya, China, April 29 – May 3, 2019. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 11458, 100-110 (2019).
Summary: In this paper, we discuss the computational complexity of read-once resolution (ROR) with respect to Horn formulas. Recall that a Horn formula is a Boolean formula in conjunctive normal form (CNF), such that each clause has at most one positive literal. Horn formulas find applications in a number of domains such as program verification and logic programming. It is well-known that deduction in ProLog is based on unification, which in turn is based on resolution and instantiation. Resolution is a sound and complete procedure to check whether a Boolean formula in CNF is satisfiable. Although inefficient in general, resolution has been used widely in theorem provers, on account of its simplicity and ease of implementation. This paper focuses on two variants of resolution, viz., read-once resolution and unit read-once resolution (UROR). Both these variants are sound, but incomplete. In this paper, the goal is to check for the existence of proofs (refutations) of Horn formulas under these variants. We also discuss the computational complexity of determining optimal length proofs where appropriate.
For the entire collection see [Zbl 1408.68013].
For the entire collection see [Zbl 1408.68013].
MSC:
| 68V15 | Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) |
| 68Q25 | Analysis of algorithms and problem complexity |
References:
| [1] | Chandrasekaran, R.; Subramani, K., A combinatorial algorithm for Horn programs, Discrete Optim., 10, 85-101, 2013 · Zbl 1284.90038 · doi:10.1016/j.disopt.2012.11.001 |
| [2] | Cormen, TH; Leiserson, CE; Rivest, RL; Stein, C., Introduction to Algorithms, 2001, Cambridge: MIT Press, Cambridge · Zbl 1047.68161 |
| [3] | Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL, pp. 238-252 (1977) |
| [4] | Dowling, WF; Gallier, JH, Linear-time algorithms for testing the satisfiability of propositional Horn formulae, J. Log. Program., 1, 3, 267-284, 1984 · Zbl 0593.68062 · doi:10.1016/0743-1066(84)90014-1 |
| [5] | Gallier, J.H.: Logic for Computer Science: Foundations for Automatic Theorem Proving. Dover Books on Computer Science, 1st edn. Dover Publications (2015) |
| [6] | Iwama, K., Miyano, E.: Intractability of read-once resolution. In: Proceedings of the 10th Annual Conference on Structure in Complexity Theory (SCTC 1995), Los Alamitos, CA, USA, June 1995, pp. 29-36. IEEE Computer Society Press (1995) |
| [7] | Liberatore, P., Redundancy in logic ii: 2CNF and horn propositional formulae, Artif. Intell., 172, 2, 265-299, 2008 · Zbl 1182.68282 · doi:10.1016/j.artint.2007.06.003 |
| [8] | Owre, S., Shankar, N.: The formal semantics of PVS, March 1999 |
| [9] | Robinson, JA; Voronkov, A., Handbook of Automated Reasoning \((2\) volume set), 2001, Cambridge: MIT Press, Cambridge · Zbl 0964.00020 |
| [10] | Robinson, JA, A machine-oriented logic based on the resolution principle, J. ACM, 12, 1, 23-41, 1965 · Zbl 0139.12303 · doi:10.1145/321250.321253 |
| [11] | Rushby, JM; Owre, S.; Shankar, N., Subtypes for specifications: predicate subtyping in PVS, IEEE Trans. Softw. Eng., 24, 9, 709-720, 1998 · doi:10.1109/32.713327 |
| [12] | Szeider, S.; Goré, R.; Leitsch, A.; Nipkow, T., NP-completeness of refutability by literal-once resolution, Automated Reasoning, 168-181, 2001, Heidelberg: Springer, Heidelberg · Zbl 0988.03020 · doi:10.1007/3-540-45744-5_13 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
