Sieg, W. and J. Byrnes, 1996, Normal Natural Deduction Proofs (in Classical Logic) 내용을 바탕으로 명제 논리 자동 증명기를 만들어봤습니다. 본문에는 술어 논리까지 설명되어 있는데, 저는 일단 명제 논리까지만 구현해뒀습니다.
(일단 계산 복잡도는 뒤로 미루고) 명제 논리는 진리표 같은 의미론적 방식으로 쉽게 검증이 가능해서 컴퓨터로 알고리즘을 구현하는 게 그리 놀라운 일은 아니긴 합니다. 하지만 저 논문에서 자연 연역 같은 구문론적 방식으로 사람이 읽을 수 있는 자동 증명을 소개하길래 신기해서 저도 직접 만들어 봤습니다. (Tableaux 자동 증명도 있긴 한데, 완전히 구문론적이라고 보기에는 좀 애매한 면이 있는 듯해서 제외했습니다.) 이 방식은 효율성이 좀 떨어지지만, 검증 과정을 사람이 읽을 수 있다는 게 아무래도 교육적으로 큰 장점인 것 같습니다. 처음에는 C++로 만들려다 정신이 나갈 것 같아서 도중에 파이썬으로 갈아탔습니다.
Fitch나 Lemmon 같은 선형 증명 방식이 아무래도 컴퓨터로 구현하기 쉽기 때문에 Fitch 방식을 채택하여 만들었습니다. 다음은 퍼스의 법칙 증명인데
이를 다음과 같이 분석해주시면 됩니다.
빨리 만들어서 확인해보는 게 목적이고 코딩을 잘하는 편도 아니라 자동으로 선을 그려주는 기능은 없습니다. 이 점은 양해해주세요.
테스트용으로 돌려본 것들 입니다.
동일률
배중률
비모순율
클라비우스의 법칙
폭발의 원리 (모순으로부터 모든 것이 따라나온다)
모든 것이 냉장고에 있는 게 아니면 어떤 것은 냉장고에 없다 (드 모르간 법칙)
프로타고라스의 딜레마 논법
사실 논문에 나온 방식을 제가 코드로 완전히 구현했다고 확신할 수는 없어서, 틀린 증명이 생성될 수도 있고 아예 증명을 생성하지 못할 수도 있습니다. 이 점은 유의해 주세요. 관심 있으신 분들은 아래 링크에서 압축 파일을 확인해 주세요.