Now I was reading a paper where somebody used
modus ponens and these two axioms:
He then claimed that this here is derivable, whereby
later in the paper he presented a derivation:
He also said its not easy to find such a proof
and that he was helped! Can Prolog help?
Maybe using something from here can help:
Meta-interpreter collection for Prolog
https://github.com/Joelbyte/verdi-neruda