증명보조기를 만드는 게 꿈인 학부생이 1차 논리 증명보조기 만든다면 나쁘진 않은 거겠죠?

제가 최근에 λ-Prolog라는 강력한 언어로,

공리꼴을 지원하는 1차 논리 증명보조기의 백엔드로 쓰일 수 있는 프로그램(

https://github.com/mecheng98/pa/blob/master/fol.mod /* 맨 아래의 example1은 배중률의 증명을 인코딩한 거에요. */

)을 만들었습니다.

올해에는 λ-Prolog까지 구현해서 1차 논리 증명보조기를 만들어보려는데, 실패하더라도 나쁘진 않은 시도겠지요?