Joseph Vidal Rosset expressed some regret that his Prolog capabilities are limited. Maybe we can pool on others Prolog programming capabilities. So here is the callenge, provide Beckert & Posegga in Prolog.
Beckert & Posegga is usually pitched as being the shortest first order logic prover around. But there is a catch, namely it needs a preparation step, the formula needs to be braught in a special form before it can be tried by the prover.
So in the end the prover will not only be the epic few lines from here, but a little more:
Anybody up to the challenge, including running the Pelletier’s problems.
And how about display found proofs?
Cross posted on Stackoverflow: