Skip to main content
Springer Nature Link
Log in

On resolution with short clauses

  • Published:
Save article
View saved research
Annals of Mathematics and Artificial Intelligence Aims and scope Submit manuscript

Abstract

We investigate properties ofk-resolution, a restricted version of resolution in which one parent clause must have length at mostk. Starting from a unit-preference strategy, we compare minimal proof lengths of unit-resolution and unrestricted resolution. In particular, we show that the speed-up by using resolution is bound by\(\sqrt t \) if the shortest unit-resolution refutation needst steps. Next we present an algorithm which decides whether the empty clause can be deduced by 2-resolution from a formula Φ and has time complexity O(length(Φ)4). Finally we describe effects onk-resolution if a formula is transformed intot-CNF and show that extended 3-resolution is complete and sound.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Subscribe and save

Springer+
from €37.37 /Month
  • Starting from 10 chapters or articles per month
  • Access and download chapters and articles from more than 300k books and 2,500 journals
  • Cancel anytime
View plans

Buy Now

Price includes VAT (Netherlands)

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

Explore related subjects

Discover the latest articles, books and news in related subjects, suggested using machine learning.

References

  1. W.F. Dowling and I.H. Gallier, Linear-time algorithms for testing the satisfiability of propositional Horn formulas,I. Logic Programming 3 (1984) 267–284.

    Google Scholar 

  2. E. Eder,Relative Complexities of First Order Calculi (Vieweg, 1992).

  3. G. Gallo and M.G. Scutellà, Polynomially satisfiability problems,Information Processing Letters 29 (1988) 267–284.

    Google Scholar 

  4. A. Haken, The intractability of resolution,TCS 39 (1985) 297–308.

    Google Scholar 

  5. H. Kleine Büning, On generalized Horn formulas andk-resolution,TCS 116 (1993) 405–413.

    Google Scholar 

  6. G.S. Tseitin, On the complexity of derivations in the propositional calculus, in:Structures in Constructive Mathematics and Mathematical Logic, Part II, ed. A.O. Slisenko (1968) pp. 115–125.

  7. L. Wos, D. Carson and G.A. Robinson, The unit preference strategy in theorem proving,AFIPS Conf. Proc. 26 (Spantau Books, Washington, DC).

  8. S. Yamasaki and S. Doshita, The satisfiability problem for a class consisting of Horn sentences and some none-Horn sentences in propositional logic,Information and Control 59 (1983) 1–12.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. NEC Research Institute, 4 Independence Way, 08540, Princeton, NJ, USA

    Michael Buro

  2. Department of Computer Science, University of Paderborn, Warburger Straße 100, 33098, Paderborn, Germany

    Hans Kleine Büning

Authors
  1. Michael Buro
    View author publications

    Search author on:PubMed Google Scholar

  2. Hans Kleine Büning
    View author publications

    Search author on:PubMed Google Scholar

Rights and permissions

Reprints and permissions

About this article

Cite this article

Buro, M., Büning, H.K. On resolution with short clauses. Ann Math Artif Intell 18, 243–260 (1996). https://doi.org/10.1007/BF02127749

Download citation

  • Issue date:

  • DOI: https://doi.org/10.1007/BF02127749

Keywords