Usage
  • 10 views
  • 3 downloads

Non-Obviousness

  • Author(s) / Creator(s)
  • Introduction: Some problems that are difficult for automated theorem provers (ATPs) are so merely because of their size, but not because of any logical or conceptual complexity. Examples of this type of difficult problem have been published in the past: see Pelletier [1986: problems 12, 29, 34, 38, 43, 51-53, 62, 66-68, and 71-74]. But there is another type of problem whose statement can be quite simple but whose proofs are nevertheless quite difficult for ATPs (and people) to find. This note gives an example of such a problem.

  • Date created
    1986
  • Subjects / Keywords
  • Type of Item
    Article (Published)
  • DOI
    https://doi.org/10.7939/R3J960Q6H
  • License
    © 1986 Francis J. Pelletier et al. This version of this article is open access and can be downloaded and shared. The original author(s) and source must be cited.
  • Language
  • Citation for previous publication
    • Pelletier, F.J., & Rudnicki, P. (1986). Non-Obviousness. Newsletter of the Association for Automated Reasoning, 6, 4-5. Retrieved from https://mystelven.github.io/Association-Automated-Reasoning/Newsletters/006-1986-09.pdf
  • Link to related item
    https://mystelven.github.io/Association-Automated-Reasoning/Newsletters/006-1986-09.pdf