질문:

공리와 목표로 구성된 문제에 대한 사양이 있다고 가정합니다 (즉, 관련된 증거 문제는 모든 공리가 주어지면 목표를 충족시킬 수 있는지 여부입니다). 또한 문제가 공리들 사이에 불일치 / 모순이 포함되어 있지 않다고 가정하자. 문제를 증명하는 데 “고차 추론”이 필요한지 미리 결정하는 방법이 있습니까 (즉, 완전한 증거를 먼저 작성하지 않고)?

“고차 추론”이란 고차 논리를 기록해야하는 증명 단계를 적용하는 것을 의미합니다. “고차 추론”의 전형적인 예는 귀납 일 것입니다 : 귀납 체계를 원칙적으로 쓰려면 고차 논리를 사용해야합니다.

예:

증명 문제를 지정할 수 있습니다. “두 개의 자연수에 대한 추가는 정류입니까?” 1 차 로직 사용 (즉, “plus”함수를 재귀 적으로 정의하는 공리와 함께 표준 공리와 함께 생성자 zero / succ를 통해 자연수를 정의) 이 문제를 증명하려면 “plus”의 첫 번째 또는 두 번째 인수의 구조에 대한 유도가 필요합니다 ( “plus”의 정확한 정의에 따라 다름). 증명하기 전에 입력 문제의 본질을 분석하여 이것을 알 수 있었습니까? (물론 이것은 설명을위한 간단한 예일뿐입니다. 실제로, 이것은 플러스의 commutativity보다 더 어려운 증명 문제에 흥미로울 것입니다.)

더 많은 맥락 :

내 연구에서, 나는 종종 뱀파이어, 이프 로버 등과 같은 자동화 된 1 차 정리 프로 버를 적용하여 증명 문제 (또는 증명 문제의 일부)를 해결하려고 시도하는데, 그 중 일부는 고차 추론이 필요할 수 있습니다. 종종, 증명 자들은 증거를 제시하는 데 꽤 많은 시간이 필요합니다 (일차 추론 기술 만 필요한 증거가 있다면). 물론, 고차 추론이 필요한 문제에 1 차 정리를 적용하려고하면 일반적으로 시간 초과가 발생합니다.

따라서 증명 문제가 고차 추론 기법을 필요로하는지 여부를 사전에 알려줄 수있는 방법 / 기술이 있는지 궁금합니다 ( “1 차 정리 증명 자에게 전달하는 데 시간을 낭비하지 마십시오”). ) 또는 그렇지 않은 경우, 적어도 특정 입력 문제 일 수 있습니다.

나는 문학에서 내 질문에 대한 답을 찾고 정리에 관한 일부 동료 연구원들에게 그 사실을 입증 해달라고 요청했지만 지금까지는 좋은 답을 얻지 못했습니다. 내 기대는 대화식 정리 증명과 자동 정리 증명 (Coq community? Isabelle community (Sledgehammer)?)을 결합하려는 사람들의 주제에 대한 연구가 있지만 지금까지는 아무것도 찾을 수 없었습니다.

나는 일반적으로 여기에 설명 된 문제가 결정 불가능한 것 같습니다 (그렇습니까?). 그러나 문제의 개선 된 버전에 대한 좋은 대답이있을 수 있습니다 …?

답변