Nqthm

Nqthm은 때때로 보이어-모어 정리라고 불리는 정리 perveron이다.ACL2의 전조였다.^[1]

역사

이 시스템은 로버트 S에 의해 개발되었다. 보이어와 J 스트로터 무어 텍사스 주립대 컴퓨터공학부 교수.그들은 1971년 스코틀랜드의 에든버러에서 이 시스템에 대한 작업을 시작했다.그들의 목표는 완전히 자동화된 논리 기반의 정리 프로베어링을 만드는 것이었다.그들은 작동 논리로 순수 LISP의 변형을 사용했다.

정의들

정의는 완전히 재귀적 함수로 형성되며, 시스템은 다시 쓸 때 사용되는 재쓰기 및 유도 휴리스틱스를 광범위하게 사용하며, 상징적 평가라고 불리는 것이 실패한다.

이 시스템은 Lisp 위에 구축되었으며 Common Lisp 구현으로 부팅한 후 기계의 상태인 "그라운드 제로"라고 불리는 것에 대한 매우 기본적인 지식을 가지고 있었다.

이것은 단순한 산술 정리의 증명 사례다.함수TIMES는 BOOT-STRAP("위성"이라 함)의 일부로서 다음과 같이 정의된다.

 (DEFN 시대 (X Y)   (IF (제로프 X)       0       (플러스 Y (시대 (SUB1 X) Y)))) 

정리정립

정리의 공식은 또한 Lisp와 같은 구문으로 주어진다.

 (증명-레마 동일률. (다시 쓰다)    (대등하다 (시대 x z) (시대 z x))) 

그 정리가 사실임이 입증되면, 시스템의 지식 기반에 추가될 것이며, 향후 증명에 대한 재작성 규칙으로 사용될 수 있다.

그 증거 자체는 준자연어법으로 주어진다.저자들은 수학적 증거에 단계를 포함시키기 위해 무작위로 전형적인 수학적 구절을 선택하는데, 이것은 실제로 그 증거를 꽤 읽을 수 있게 만든다.Lisp 구조를 다소 읽기 쉬운 수학적 언어로 변형시킬 수 있는 LaTeX용 매크로가 있다.

시간의 일치성에 대한 증거는 다음과 같이 계속된다.

추측에 *1이라는 이름을 붙이시오.우리는 인덕션에 호소할 것이다.추측에서 두 가지 유인이 제시되는데, 두 가지 모두 흠이 있다.우리는 우리의 고려를 추측에서 가장 많은 수의 비원리적 재귀적 함수에 의해 제안된 두 개로 제한한다.이 두 가지 모두 가능성이 같기 때문에 우리는 임의로 선택할 것이다.우리는 (AND (ZEROP X) (p X Z) (AND (ZEROP X) (P X Z) (AND (NOT (ZEROP X) (p (SUB1 X) Z) (p X Z)))) (P X Z))) (AND (AND)))) (P X Z)))에 따라 유도할 것이다.선형 산술, 보조정리 CACK-NUMP 및 ZEROP의 정의는 계획의 각 유도 단계에서 근거 있는 관계 LESP에 따라 측정치(Count X)가 감소함을 알려준다.위의 유도 계획은 다음과 같은 두 가지 새로운 추측을 낳는다.사례 2. (IMPies(ZEROP X) (EQUAL(TIMES X Z)(TIMES Z X)))) 

그리고 수많은 유도증거들을 훑어본 후, 마침내 다음과 같이 결론짓는다.

사례 1. (IMPies (AND (NOT (ZEROP Z))) (EQUAL 0 (TIMES (SUB1 Z) 0))) (EQUAL 0 (TIMES Z 0))))이를 통해 ZEROP, TIME, PLUS, EQUE의 정의를 다음과 같은 T로 확장하여 단순화한다.그것은 *1. Q.E.D. [ 0.0 1.2 0.5 ] Commutativity-OF-TIME의 증명도 마무리한다.

교정쇄

특히 이 시스템을 통해 많은 증거가 작성되거나 확인되었다.

• 목록 연결
• 삽입 정렬
• (iii) 이항 첨가제
• (iii) 스택 시스템의 식 컴파일러
• (iiii) 주요 인자의 고유성
• (1983) RSA 암호화 알고리즘의 역직성
• (1984) 순수 리스에 대한 정지 문제의 불능성
• (1985) FM8501 마이크로프로세서(워렌 헌트)
• (1986) 괴델의 불완전성 정리(상카르)
• (1988) CLI 스택(Bill Bevier, Warren Hunt, Matt Kaufmann, J Moore, Bill Young)
• (1990) 가우스의 이차적 상호주의 법칙 (David Russinoff)
• (1992) 비잔틴 장군 및 시계 동기화 (베비에르와 영)
• (1992) Nqthm 언어의 서브셋에 대한 컴파일러(Arthur Platau)
• (iii-phase 마크 비동기 통신 프로토콜)
• (1993) 모토로라 MC68020 및 버클리 C 스트링 라이브러리(위안유)
• (1994) 파리-해링턴 램지 정리 (케네스 쿠넨)
• (1996) NFSA와 DFSA의 동등성 (Debora Weber-Wulff)

PC-Nqthm

PC-Nqthm(Proof-Checker Nqthm)이라고 불리는 보다 강력한 버전이 Matt Kaufmann에 의해 개발되었다.이를 통해 시스템이 자동으로 사용하는 증명 도구를 사용자에게 제공함으로써 증명에 대한 더 많은 지침을 제공할 수 있게 되었다.이 제도는 귀납적 증거의 무한 사슬을 헤매는 비생산적인 경향을 가지고 있기 때문에 이것은 큰 도움이 된다.

문학

• 1997년 제2판 학술 출판사, R.S.보이어와 J.S.무어 컴퓨터 논리 핸드북.
• M. Kaufmann과 R. S. Boyer, Computer and Mathical with Applications, 29(2), 1995, 페이지 27–62로 구성된 Boyer-Moore Organization Prover와 그것의 상호작용 강화.

수상

상

2005년 로버트 S. 보이어, 맷 카우프만, J 스트로터 무어는 Nqthm 정리 프로베른에 대한 연구로 ACM 소프트웨어 시스템 상을 받았다.^[3]

참조

외부 링크

• 자동추론시스템, Nqthm
• 보이어-모어 정리 프로베라 (NQTHM)
• 시스템이 더 이상 지원되지 않더라도 [1]에서 사용할 수 있다.
• GitHub에서 실행 가능한 버전: [2]