論理計算と随伴関手(1)

論理プログラミングの説明でプログラムの実行を逆にたどると証明になるという説明をしようとしましたが、説明はなかなか難しいです。随伴関手の考え方で説明できるかもしれないと思いますので、説明できれば説明してみたいと思います。