The following construct provides a kind of pseudo-negation meaning “P is not provable”. This is not real negation (“P is false”). The following two goals are equivalent:
\+ P (P -> fail ; true)