Abstract
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.
The first author was supported in part by the National Science Foundation through Award CCF-1305054.
This research was made possible by NASA WV EPSCoR Grant # NNX15AK74A.
The second author was supported in part by the Air Force Research Laboratory under US Air Force contract 88ABW-2017-1077.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsReferences
Chandrasekaran, R., Subramani, K.: A combinatorial algorithm for Horn programs. Discrete Optim. 10, 85–101 (2013)
Cormen, T.H., Leiserson, C.E., Rivest, R.L., Stein, C.: Introduction to Algorithms. MIT Press, Cambridge (2001)
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)
Dowling, W.F., Gallier, J.H.: Linear-time algorithms for testing the satisfiability of propositional Horn formulae. J. Log. Program. 1(3), 267–284 (1984)
Gallier, J.H.: Logic for Computer Science: Foundations for Automatic Theorem Proving. Dover Books on Computer Science, 1st edn. Dover Publications (2015)
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)
Liberatore, P.: Redundancy in logic ii: 2CNF and horn propositional formulae. Artif. Intell. 172(2), 265–299 (2008)
Owre, S., Shankar, N.: The formal semantics of PVS, March 1999
Robinson, J.A., Voronkov, A.: Handbook of Automated Reasoning (\(2\) volume set). MIT Press, Cambridge (2001)
Robinson, J.A.: A machine-oriented logic based on the resolution principle. J. ACM 12(1), 23–41 (1965)
Rushby, J.M., Owre, S., Shankar, N.: Subtypes for specifications: predicate subtyping in PVS. IEEE Trans. Softw. Eng. 24(9), 709–720 (1998)
Szeider, S.: NP-completeness of refutability by literal-once resolution. In: Goré, R., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS, vol. 2083, pp. 168–181. Springer, Heidelberg (2001). https://doi.org/10.1007/3-540-45744-5_13
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2019 Springer Nature Switzerland AG
About this paper
Cite this paper
Kleine Büning, H., Wojciechowski, P., Subramani, K. (2019). Read-Once Resolutions in Horn Formulas. In: Chen, Y., Deng, X., Lu, M. (eds) Frontiers in Algorithmics. FAW 2019. Lecture Notes in Computer Science(), vol 11458. Springer, Cham. https://doi.org/10.1007/978-3-030-18126-0_9
Download citation
DOI: https://doi.org/10.1007/978-3-030-18126-0_9
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-18125-3
Online ISBN: 978-3-030-18126-0
eBook Packages: Computer ScienceComputer Science (R0)