규칙 재작성 데이터베이스 구축: 야심찬 프로젝트

이 게시글에서는 정수 속성, 미분, 집합 이론, 비트 벡터, 함수형 프로그램 등 다양한 영역을 포괄하는 규칙 재작성 데이터베이스를 만드는 것을 제안합니다. 저자는 규칙 재작성을 포함하는 기존 프로젝트와 라이브러리를 다수 나열하고, 이러한 규칙들을 공통 형식으로 통합하는 것의 실현 가능성과 과제에 대해 논의합니다. 일부 규칙은 기존 SMT 솔버를 사용하여 직접 증명할 수 있지만, 저자는 특정 애플리케이션 컨텍스트에서 정확한 재작성 및 조작을 위해 명확하게 정의된 규칙 재작성 데이터베이스가 필수적이며, 미래 연구에 귀중한 자원이 될 것이라고 주장합니다.