Prolog라는 논리형 프로그래밍 언어가 있다.
수리논리와 집합론을 공부하는 중에
정주희 교수님이 Proofmood라는 증명확인기계를
구현하신 걸 보고 나도 만들어보고 싶었다.
그런데 Prolog로 공리계를 코딩하면 인터프리터가
식이 공리계를 만족하는지를 증명하므로,
이걸로 구현할 수 있을 것 같았고
몇 가지 케이스에 대해서는 잘 돌아갔다.
그러나 Prolog 인터프리터는 DFS( 깊이우선탐색 )을
사용하므로 무한루프에 빠져버리는 경우가 있었다.
그래서 나는 Prolog를 개선한 언어를 만들고 싶다.
1. 인터프리터가 DFS를 사용하지 않을 것.
2. 타입을 두어 그 타입의 모든 값에 대하여 탐색할 것.

이제 나만의 언어 Butterfly를 소개하겠다.
타입은 생성자의 집합이며 대상영역과 대응된다.
n항 생성자는 값 n개와 결합하여 타입의 값이 되고,
함수 또는 상수에 대응된다.
변수는 항으로 치환될 수 있다.
항은 변수이거나 생성자와 항의 결합이다.
식은 술어와 항의 결합이고,
변수 배정은 식에 있는 변수를 값으로 치환한다.
공리는 "임의의 변수 배정이 주어졌을 때,
(어떤 논리식들의 집합)의 원소가 모두 참이면
(어떤 논리식)이 참이다."의 꼴 뿐이다.
그리고 인터프리터에 식을 주면 어떤 변수 배정에서 그 식이 공리계로부터 유도될 수 있는지를 답한다.

연약해보이지만 이걸로 명제논리에서의 증명
→ Sigma proves phi
이 존재하는지를 알 수 있다.

이제 구현이 문제인데,
지금 생각해둔 건 뉴런에서 힌트를 얻은 것이다.
ㅂㅅ같게도 약간 Dimer스럽다.
0개 이상의 입력돌기와 1개의 출력돌기를 가진 뉴런은 어떤 공리와 대응되며 입력돌기는 그 공리의 머리 부분, 출력돌기는 꼬리 부분에 대응된다.
각 돌기는 점에서 만나며,
각 점은 고유한 술어에 관한 식의 집합- 공집합으로 초기화됨 -을 가지고 있다.
이때 필요한 기술이 식의 집합 Phi와 식 psi가
주어졌을 때, psi[x := t] in Phi인 변수 x와 항 t의 순서쌍의 집합을 찾아내는 법이다.
이때 순서쌍 (x, t)가 psi에 대응하는 입력돌기를 활성화시킨다고 하자.
모든 입력돌기를 활성화시키는 순서쌍의 집합의 각 원소에 대응하는 적절한 식들을 뉴런은 매 순간마다 출력돌기에서 출력한다.

더 좋은 방법이 있으면 알려주세요. 제발 ㅠㅠ
이거 구현하고 과제 날로 먹고싶은 마음은 없지 않습니다.