PENG
Processable ENGlish

Example Specification

Dreadsbury Mansion Mystery in English

[J. F. Pelletier, Seventy-Five Problems for Testing Automatic Theorem Provers, Journal of Automated Reasoning 2(2), pp. 191-216, 1986]

  1. Someone who lives in Dreadsbury Mansion killed Aunt Agatha.
  2. Agatha, the butler, and Charles live in Dreadsbury Mansion, and are the only people who live therein.
  3. A killer always hates his victim, and is never richer than his victim.
  4. Charles hates no one that Aunt Agatha hates.
  5. Agatha hates everyone except the butler.
  6. The butler hates everyone not richer than Aunt Agatha.
  7. The butler hates everyone Aunt Agatha hates.
  8. No one hates everyone.
  9. Agatha is not the butler.
Therefore: Agatha killed herself.

Dreadsbury Mansion Mystery in PENG

  1. A person who lives in Dreadsbury Mansion kills Agatha.
  2. Agatha lives in Dreadsbury Mansion.
  3. The butler lives in Dreadsbury Mansion.
  4. Charles lives in Dreadsbury Mansion.
  5. If a person lives in Dreadsbury Mansion then the person is Agatha or is the butler or is Charles.
  6. If a person X kills a person Y then the person X hates the person Y.
  7. If a person X kills a person Y then the person X is not richer than the person Y.
  8. If Agatha hates a person then Charles does not hate the person.
  9. If a person is not the butler then Agatha hates the person.
  10. If a person is not richer than Agatha then the butler hates the person.
  11. If Agatha hates a person then the butler hates the person.
  12. No person hates every person.
  13. Agatha is not the butler.
Who kills Agatha?
Does the butler kill Agatha?
Does Agatha kill Agatha?

[Back]

© Rolf Schwitter, Macquarie University, Australia
Last modified: 28th February 2007