Sieg, W. and J. Byrnes, 1996, Normal Natural Deduction Proofs (in Classical Logic) 내용을 바탕으로 명제 논리 자동 증명기를 만들어봤습니다. 본문에는 술어 논리까지 설명되어 있는데, 저는 일단 명제 논리까지만 구현해뒀습니다.
(일단 계산 복잡도는 뒤로 미루고) 명제 논리는 진리표 같은 의미론적 방식으로 쉽게 검증이 가능해서 컴퓨터로 알고리즘을 구현하는 게 그리 놀라운 일은 아니긴 합니다. 하지만 저 논문에서 자연 연역 같은 구문론적 방식으로 사람이 읽을 수 있는 자동 증명을 소개하길래 신기해서 저도 직접 만들어 봤습니다. (Tableaux 자동 증명도 있긴 한데, 완전히 구문론적이라고 보기에는 좀 애매한 면이 있는 듯해서 제외했습니다.) 이 방식은 효율성이 좀 떨어지지만, 검증 과정을 사람이 읽을 수 있다는 게 아무래도 교육적으로 큰 장점인 것 같습니다. 처음에는 C++로 만들려다 정신이 나갈 것 같아서 도중에 파이썬으로 갈아탔습니다.
Fitch나 Lemmon 같은 선형 증명 방식이 아무래도 컴퓨터로 구현하기 쉽기 때문에 Fitch 방식을 채택하여 만들었습니다. 다음은 퍼스의 법칙 증명인데
이를 다음과 같이 분석해주시면 됩니다.
빨리 만들어서 확인해보는 게 목적이고 코딩을 잘하는 편도 아니라 자동으로 선을 그려주는 기능은 없습니다. 이 점은 양해해주세요.
테스트용으로 돌려본 것들 입니다.
동일률
배중률
비모순율
클라비우스의 법칙
폭발의 원리 (모순으로부터 모든 것이 따라나온다)
모든 것이 냉장고에 있는 게 아니면 어떤 것은 냉장고에 없다 (드 모르간 법칙)
프로타고라스의 딜레마 논법
사실 논문에 나온 방식을 제가 코드로 완전히 구현했다고 확신할 수는 없어서, 틀린 증명이 생성될 수도 있고 아예 증명을 생성하지 못할 수도 있습니다. 이 점은 유의해 주세요. 관심 있으신 분들은 아래 링크에서 압축 파일을 확인해 주세요.
12개의 좋아요
윈도에서 실행할 수 있는 이진 파일이 이 압축 파일 안에 있나요?
네, 링크에 들어가서 압축을 푼 뒤 ND_Proof를 실행하시면 됩니다. 가끔 처음 실행하면 ‘인식할 수 없는 앱의 시작을 차단했습니다’ 같은 경고 창이 뜰 수도 있는데, 이상한 건 없으니 안심하시고 추가 정보를 누른 뒤 실행하시면 돼요.
오늘 확인해 보니, 어떤 증명들은 틀린 것은 아니지만 불필요한 규칙을 많이 시도하더라고요. 고칠 수 있으면 고쳐 보고 싶은데, exe로 배포하는 방식이다 보니 수정할 때마다 새 파일을 다시 공유해야 해서 조금 번거롭네요.
https://www.umsu.de/trees/
그래서 나중에 천천히, 위 링크처럼 다운로드 없이 웹에서도 사용할 수 있도록 만들어 볼까 생각 중입니다. 만약 만들게 된다면 피치 스타일이 아닌 겐첸식 트리 방식으로 만들어보고 싶네요.
2개의 좋아요
https://coffeeandnotes005-lgtm.github.io/natural-deduction-prover/
이번에 새로 만들어본 술어논리 버전입니다. 겐첸식 자연연역으로 만들려고 했으나 생각보다 어려워서 그냥 피치식을 깔끔하게 나타내는 방식으로 만들었습니다.
이건 음주자 역설을 입력하여 나온 결과입니다. 특이한 형태의 증명이 나왔네요.
아쉽게도 동일성과 연산은 지원되지 않습니다. 연산기호는 추가할 수 있었지만 동일성이 없으면 큰 의미가 없을 것 같아서 그냥 제외했습니다. 동일성 규칙을 어떻게 다뤄야 될지 아직까지는 잘 모르겠습니다.
증명 탐색이 10초를 넘기면 그냥 증명을 포기하게 만들었습니다. 처음에는 시간이 오래 걸려도 계속 시도하게 만들었었는데, 그러다 보면 페이지 연결이 끊기더라고요. 그래서 그냥 제한 시간을 걸어뒀습니다. 때문에 증명을 생성하지 못하는 경우도 많습니다. 전제가 복잡할 경우 자주 이러더군요.
실용적인 목적으로 만든 것은 아니고 순수한 호기심 때문에 만든 것이라 이후 큰 개선은 없을 것 같아요. 그냥 이 정도에서 만족하고 끝내려 합니다 ㅎㅎ
2개의 좋아요
