를 만들고 싶은데, 구현하기에 앞서 설계하는 것부터 잘 안 되네요.

등호 소거 규칙이나 공리꼴 변수를 인스턴스화하는 데 필요한 기술은 확보해뒀습니다.


문제는 대화형이면서 자연연역 기반으로 만드는 게 너무 어렵다는 거에요.

대화형 증명보조기인 Coq는 탑-다운 방식인데,

겐첸의 자연연역은 바텀-업 방식이잖아요.

그래서 Coq를 모방해도 자연연역 기반의 대화형 증명보조기를 만들긴 어려운 것 같아요.

그렇다고 대화형이 아니면, 이미 유명한 Fitch 시스템이랑 다른 게 없을 것 같고요.

좋은 아이디어 있으신 분 계신가요??