Unrestricted resolution versus N-resolution

  • Andreas Goerdt
Part of the Lecture Notes in Computer Science book series (LNCS, volume 452)


An N-resolution proof is a resolution proof in which the resolution rule is restricted: One clause to which it is applied must only consist of negative literals. N-resolution is complete. ([8], p. 109,


Propositional Variable Pigeonhole Principle Partial Truth Critical Extension Empty Clause 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [1]
    M. Ajtai, The complexity of the propositional pigeonhole principle, Proc. of the IEEE FOCS (1988).Google Scholar
  2. [2]
    S. R. Buss and G. Turán, Resolution proofs of generalized pigeonhole principles, Theoret. Comp. Sci. 62 (1988) 311–317.Google Scholar
  3. [3]
    V. Chvátal and E. Szemeredi, Many hard examples for resolution, J. Assoc. Comput. Mach. 35(4) (1988) 759–768.Google Scholar
  4. [4]
    A. Goerdt, Davis Putnam resolution versus unrestricted resolution, Journal of Discrete Applied Mathematics, Special issue on proof lengths, accepted for publication.Google Scholar
  5. [5]
    A. Goerdt, Regular resolution versus unrestricted resolution, Technical report, Univ. of Duisburg, submitted.Google Scholar
  6. [6]
    A. Haken, The intractability of resolution, Theoret. Comput. Sci. 39 (1985) 297–308.Google Scholar
  7. [7]
    J. A. Robinson, Automatic deduction with hyper-resolution, (1965), in [11] vol. 1, 416–423.Google Scholar
  8. [8]
    U. Schöning, Logik für Informatiker, BI-Taschenbuch, Reihe Informatik 56 (Bibliographisches Institut, Mannheim, 1987).Google Scholar
  9. [9]
    M. E. Stickel, An introduction to automated deduction, Fundamentals of artificial intelligence (Bibel, Jorrand eds.), Lect. Notes of Comp. Sci. 132 (Springer Verlag, Berlin, 1986) 75–137.Google Scholar
  10. [10]
    M. E. Stickel, A PROLOG technology theorem prover: Implementation by an extended PROLOG compiler, J. of Automated Reasoning 4 (1988) 353–380.Google Scholar
  11. [11]
    J. Siekmann, G. Wrightson (eds.), Automation of reasoning — classical papers on computational logic, vol.1 and 2, Springer (1983).Google Scholar
  12. [12]
    G. A. Wilson, C. Minker, Resolution, refinements and search strategies: A comparative study, IEEE Transactions on Computers C-25 (1976).Google Scholar
  13. [13]
    A. Urquhart,Hard examples for resolution, J. Assoc. Comput. March 34 (1987), 209–219.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1990

Authors and Affiliations

  • Andreas Goerdt
    • 1
  1. 1.Universität -GH- Duisburg, FB 11, Praktische InformatikDuisburgWest-Germany

Personalised recommendations