대 시도를 실행할 때 내가 (이이 제목에 언급되지 않음) 슬레지 해머 결과에서 는 의 출력이 실행하는 동안 종종 쇠망 에서 다양한 결과를 제공하려고 만 보면 이유는 완전히 다른 결과를 얻을 수 있습니까 슬레지 해머가 직접 제로 (!) 결과를줍니다.이사벨 : 쇠망
이제 슬레지 해머의 디자인 목표는 결정론이 아닙니다. as stated by Lawrence Paulson. 그러나이 무작위적인 결과는 왜 이 초보자에게는 약간의 낙담점인지, 내게는 뿐 아니라 프로젝트에서 도움이되는 학생에게도 도움이되지 않습니다.
항상 Sledgehammer를 실행하고 병렬로 시도하는 것이 좋습니다.
정확한 답변이 필요하지 않지만 누구나 결과가 다를 수 있다는 단서가 있습니까? 두 개의 쇠망 치는 전화가 다른 매개 변수를 특징으로합니까?
먼저 Isabelle 사용자의 메일 링리스트에 가입하여 이러한 정보에 대한 정보를 확인하시기 바랍니다. 특히, 지난 6 개월, 쇠 망치 sledgehammer이 try와 어떻게 연관되는지를
Isabelle/Options의 Auto methods가 try와 어떻게 연관되는지를try에 영향을 미치는 sledgehammer,sledgehammer,sledgehammer 출력에 영향을주는 두 개의 큰 가지 옵션과 멀티 스레딩, 당신은 완전히에게 옵션을 제공하여 sledgehammer 옵션을 제어 할 수 있다는 것입니다 귀하의 질문에 관련이사용하거나 sledgehammer-params을 사용하여 옵션을 설정하십시오.
다음은 M.Wenzel이 어제 Sledgehammer의 자동 설정에 대한 간단한 설명을 주었던 메일 링리스트에 대한 링크입니다.
두 번째 질문에 대한 또 다른 대답은 다음과 같습니다. try 명령은 try0과 sledgehammer의 멀티 스레드 조합입니다. 기본 sledgehammer 옵션이 있으며 sledgehammer_param으로 볼 수 있습니다. 이 옵션을 변경하지 않았다면 이론에 사용 된 sledgehammer 명령은이 옵션을 사용합니다. try이이 옵션을 사용하는지 여부는 알 수 없지만 try이 sledgehammer에 기본 옵션에없는 증명기를 제공하는지 여부를 확인하는 방법을 알려 드리겠습니다.
나는 그것이 나를 위해 일하는 것처럼 try이 당신을 위해 일한다고 가정합니다.
먼저 sledgehammer_params을 삽입하고 출력 패널을 확인하십시오. provers이 표시됩니다. 내가 코어 4 개를 가지고 있기 때문에 나의 디폴트는 e spass vampire z3이다. 이들은 PIDE가 시작할 때 선택되었습니다. 이들은 Sledgehammer 패널에 표시되는 것과 동일한 보호 기능입니다. 두 번째로 중요한 옵션은 timeout = 30입니다.
try0 방법을 증명할 수있는 정리에 대한
try를 삽입
및 sledgehammer, 출력 패널에 표시되는 각 by 증거와 함께, 그것은 나에게 발견 된 ATP (자동 정리의 증명)를 말할 것입니다 수 증명. 예를 들어, 내게는 "e", "z3" 및 "spass"이 표시되며 각각 뒤에 증거가 표시됩니다.
답변 : sledgehammer_params를 사용하면 목록에없는 ATP를 보여줍니다try 경우, try이 기본 옵션으로 sledgehammer 실행할 때와 다른 provers 옵션 sledgehammer을주고있다.
나열하려고 입증 자 실행 :을 당신이 당신을 제공 try, try 나열된 개별 피 인증을 실행하는 것과 같은 sledgehammer 증거를 제공하기 위해 sledgehammer를 얻을 수 있는지에 대한 질문에 대답하기 위해, 예를 들어 다음과 같이 :
sledgehammer[provers = "z3", timeout = 60]
나는 timeout 그냥 당신이 그것을 바꿀 수 있다는 것을 보여 보여 주지만, try 영원히 일을하려고하지 않기 때문에 일반적으로 더 긴 제한 시간이 필요하지 않을 것입니다. try가 당신에게 z3 증거를 제공 한 경우
sledgehammer의 명시 적 사용이 당신에게
z3 증거를 제공하는 경우
, 다음이는 다른 결과에 영향을주는 옵션 및 멀티 스레딩의 있음을 알려줍니다. sledgehammer과 nitpick의 출력이 크게 다릅니다.
나는 try을 사용하지 않습니다. try0과 sledgehammer을 사용하고 있지만 자동 메소드에 대해 자동으로 설정된 옵션이 더 좋다는 것을 보여줍니다. 자동 nitpick은 nitpick의 옵션을 변경했기 때문에 nitpick이 발견되지 않는 반례를 찾습니다.
링크