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초를 넘기면 그냥 증명을 포기하게 만들었습니다. 처음에는 시간이 오래 걸려도 계속 시도하게 만들었었는데, 그러다 보면 페이지 연결이 끊기더라고요. 그래서 그냥 제한 시간을 걸어뒀습니다. 때문에 증명을 생성하지 못하는 경우도 많습니다. 전제가 복잡할 경우 자주 이러더군요.
실용적인 목적으로 만든 것은 아니고 순수한 호기심 때문에 만든 것이라 이후 큰 개선은 없을 것 같아요. 그냥 이 정도에서 만족하고 끝내려 합니다 ㅎㅎ
4개의 좋아요
아, 이건 반증은 못 하나요? 타당하지 않은 증명 목표를 제가 일부러 제시해 보니, 이 증명기가 그냥 "증명을 제한 시간 안에 생성하지 못했다."라고 답하네요.
1개의 좋아요
네, 아쉽게도 반증은 못 합니다ㅠ
Sieg, W. and J. Byrnes, 1996, Normal Natural Deduction Proofs (in Classical Logic) 에서 반증을 제시하는 법까지 알려주긴 합니다.
대략적인 원리는 주어진 결론으로부터 역방향, 전제로부터 정방향으로 가지가 열리면서, 증명 탐색이 실패한 경우는 N, 성공한 부분은 Y로 나타냅니다. Y가 확인되면 그 트리에서 자연연역을 추출합니다. N이 나오면 N으로 닫힌 가지를 이용해 반증을 제시해줄 수 있다고 설명되어 있습니다.
근데 제 증명기에서 제외한 이유는
1)증명 탐색을 위한 가지가 너무 많이 열리는 경우, Y로 닫히는 가지를 찾다가 페이지 연결이 끊겨버립니다. 가지 전체가 N으로 닫혔다는 것을 확인해야 반례를 제시해주는데, 그러다 자꾸만 멈춰버리는 상황이 많습니다.
2)그냥 제 순수 코딩 역량 문제입니다. 가지가 빨리 닫히고 끝나는 증명에 한해서 반례를 제시해준다든가 그냥 반례 탐색만 다른 방식으로 해볼까 고민은 했었는데, 솔직히 어떻게 해야 할지 감이 안 잡힙니다. 그냥 이런 게 진짜로 되나 테스트만 해보고 싶어서 만든 거라, 빨리 만들고 싶은 욕심 때문에 논문의 모든 부분을 반영하지는 않았습니다.
현재 부실한 점이 꽤 많습니다. 좀 더 다듬어보고 싶기는 한데, 자연연역 기반 자동증명에 대한 자료 구하기가 힘드네요. 그래서 이 정도에서 만족할려고요.
1개의 좋아요
복잡한 명제들의 반례를 찾고 싶으시면 이걸 추천드려요.
https://prover9.org/webapps/combo/
브라우저에서 실행할 수 있는 Prover9인데, 왼쪽 위 Prover9을 Mace4로 변경하시고 타당하지 않은 경우를 입력하시면
간단한 예)
formulas(assumptions).
exists x F(x).
end_of_list.
formulas(goals).
all x F(x).
end_of_list.
그럼 다음과 같은 모델을 찾아줘요.
1개의 좋아요
표준적인 명제 및 술어논리는 완전성이 성립하니, 런타임 초과 시 P -> ⊥이 증명 가능한지 확인하는 절차를 수행함으로써 P의 부당성을 보여주는 알고리즘을 설계하시는 것도 하나의 방법일 것 같네요.
2개의 좋아요
