안녕 얘들 아 내가 2 알고리즘을 비교하려고하고 내가 그들에 대한 증거를 시도하고 작성할 수 있습니다 생각! 우리가 알고리즘에 대한 증명 작성
같은 질문을받을 것입니다 우리의 수학 수업 작년에 일반적으로(내 수학이 너무 따라서 질문을 짜증이) 증명 : (2R + 3) = N (N + 4) 다음
내가 필요한 4 단계를 수행하고 끝에 대답을 얻을 것입니다
내가 갇혀 오전 어디 prims과 Kruskals을 증명입니다 - 내가 어떻게 진행할 수있는 위의 수학적 인 같은 형태로 이러한 알고리즘을 얻을 수
참고 : 나는 ans에 사람들에게 묻지 않습니다. 나를 위해 그것을 WER - 그냥이 자신에게
감사
당신은 많은 세부 사항을 제공하지 않지만 수학자의 사회가 갈 가질 수있는 날 형태로 그것을 얻을 수 있도록 (수학 지식 관리 MKM) 누가 수학에 대한 컴퓨터 교정을 지원하는 도구를 개발 했습니까?
및 (막연) 유니 나는 나의 수학 수업에서 최신 회의
을 프림 증명 기억하고 Kruskals 알고리즘 - 당신은 공격하지 않는다 : 예를 들어, 참조 그것을 수학적 형태로 써서. 대신, 당신은 그래프에 대한 검증 된 이론을 취해이를 결합합니다. 증거를 구축하려면 http://en.wikipedia.org/wiki/Prim%27s_algorithm#Proof_of_correctness.
복잡성을 증명하고자한다면 알고리즘의 작동으로 간단히 O (n^2)입니다. 그래프가 희소하여 O (nlogn)로 줄일 수있는 특수한 경우에 대한 최적화가 있습니다. 내가 끼 었어
는 프림과 Kruskals 증명 - 내가 어떻게 내가 당신이 할 수 있다고 생각하지 않습니다
증명하기 위해 내가 진행할 수 있도록 위의 mathmatical 것과 같은 형태로 이러한 알고리즘을 얻을 수 있습니다 직접. 대신에 두 가지가 모두 MST를 생성하고 두 개의 MST가 동일하다고 증명할 수 있습니다 (또는 일부 그래프에 대해 둘 이상의 MST를 가질 수 있기 때문에 동등한 것임을 증명하십시오). 두 알고리즘이 동등한 것으로 표시된 MST를 생성하면 알고리즘은 동일합니다.
알고리즘의 정확성을 증명하려면 일반적으로 (a) 종료되어야하고 (b) 출력이 수행하려는 작업의 사양을 충족해야 함을 보여야합니다. 이 두 가지 증명은 당신이 당신의 질문에서 언급 한 대수 증명과는 다소 다른 것입니다. 필요한 핵심 개념은 mathematical induction입니다. (증명을 위해 recursion입니다.)
예를 들어 quicksort을 봅시다.
당신이 먼저 길이 1의 입력을 종료 것을 보여 것, 그 퀵 항상 종료 증명하기 위해 (이 하찮게 사실이다.) 다음 표시가 N에 길이까지의 입력 종료되면, 그때는 것이다 길이 n + 1의 입력으로 종료하십시오. 유도 덕분에 알고리즘을 모든 입력에 대해 종료한다는 것을 증명하기에 충분합니다.quicksort가 정확한지 증명하려면 비교 정렬 지정을 정확한 수학 언어로 변환해야합니다. 우리는 출력은 상기 입력의 permutation 될 것인지 다음 I ≤ J J I ≤ 경우. quicksort의 출력이 입력의 순열이라는 것을 증명하는 것은 입력으로 시작하여 요소를 바꿔주기 때문에 쉽습니다. 두 번째 속성을 증명하는 것은 다소 까다 롭지 만 다시 유도를 사용할 수 있습니다.
대부분의 경우 증명은 손에있는 문제에 달려 있습니다. 간단한 인수은 때때로 충분할 수 있습니다. 다른 시간에 은 엄격한 증명이 필요할 수도 있습니다. 한 번 사용한 결과와 이미 증명 된 정리의 증거는 내 알고리즘이 옳다는 것을 정당화합니다. 그러나 그것은 대학 프로젝트를위한 것입니다.
아마 반자동 증명 방법을 시험해보고 싶을 것입니다. 예를 들어, Prim 및 Kruskal의 알고리즘에 대한 Java 사양이 있고 동일한 그래프 모델을 최적으로 구축하는 경우 KeY Prover을 사용하여 알고리즘의 동등성을 증명할 수 있습니다.
중요한 부분은 동적 로직 (Java 프로그램의 유형 및 기호 실행 수단을 사용한 1 차 로직의 확장)에서 증명 의무를 공식화하는 것입니다.
\forall Graph g. \exists Tree t.
(<{KRUSKAL_CODE_HERE}>resultVar1=t) <-> (<{PRIM_CODE_HERE}>resultVar2=t)
이 모든 그래프에 대한 두 알고리즘을 종료하고 결과는 같은 나무라고 표현 : 증명하는 공식은 다음 (스케치) 패턴과 일치 할 수있다.
수식 (및 알고리즘 구현)이 맞다면 Keys가 자동으로이를 증명할 수 있습니다. 그렇지 않다면 이전의 증명 트리를 검사해야하는 수량화 된 변수를 인스턴스화해야 할 수도 있습니다.
KeY로 증명 된 후에 KeY 증명에서 수동 증명을 재구성하려고하면 행복 할 수 있습니다. KeY는 Java에 대한 많은 규칙을 알고 있기 때문에 지루한 작업이 될 수 있습니다. 이해하기 쉽지 않다. 그러나, KeY가 증명에서 sequents의 오른쪽에 실존 적 한정어를 인스턴스화하는 데 사용했던 용어에서 Herbrand 분리를 추출하는 것과 같은 것을 할 수 있습니다.
글쎄, 나는 키가 재미있는 도구입니다 많은 사람들이 그와 같은 도구를 사용하여 중요한 자바 코드를 증명하기 위해 익숙해해야한다고 생각;)
KEY에서 Prim 또는 Kruskal의 알고리즘을 입증했다면,보고 싶습니다! 나는 어떤 증명 조력자도 그러한 것들에 적합하다고 믿지 않습니다. – user21820
이 mathoverflow.com을 시도합니다. 나는 당신이 더 많은 행운을 가질 것이라고 생각한다. – Toad
나는 이런 종류의 질문이 mathoverflow.com에 대한 것이라고 생각하지 않는다. –