Perguntas com a marcação «proof-techniques»

7
Invariante para loop aninhado no programa de multiplicação de matrizes

Estou fazendo uma tese de pós-graduação sobre a comprovação da correção do programa para multiplicar 2 matrizes usando a lógica Hoare. Para fazer isso, preciso gerar o loop invariável para aninhado para este programa: for i = 1:n for j = 1:n for k = 1:n C(i,j) = A(i,k)*B(k,j) + C(i,j); end...

7
Nós de baixo grau em gráficos esparsos

Deixei G = ( V, E)G=(V,E)G = (V,E) ser um gráfico tendo nnn vértices, nenhum dos quais está isolado, e n - 1n-1 1n−1 bordas, onde n ≥ 2n≥2n \geq 2. Mostre queGGG contém pelo menos dois vértices de grau um. Eu tentei resolver esse problema usando a propriedade ∑v ∈ Vdeg( v ) = 2 |...

7
Loop invariável para um algoritmo

Eu desenvolvi o seguinte pseudocódigo para o problema da soma dos pares: Dada uma matriz de números inteiros e um número inteiro , retorne YES se houver posições i, j em A com A [i] + A [j] = b , NO caso contrário.AAAbbbi,ji,ji,jAAAA[i]+A[j]=bA[i]+A[j]=bA[i] + A[j] = b Agora devo declarar um...

7
Qual é o objetivo de interpretar elementos na prova de redução do PCP ao problema de decidibilidade da validade da lógica de predicados?

Como minha pergunta se relaciona diretamente a uma parte do texto de um livro de 2004, Lógica em Ciência da Computação: Modelagem e Raciocínio sobre Sistemas (2ª Edição), de Michael Huth e Mark Ryan , para fornecer contexto para a discussão a seguir, citando parcialmente o livro literalmente: O...