Please enable JavaScript.

Coggle requires JavaScript to display documents.

Proofs - Coggle Diagram

- - - - Se a OP for atendida, ela é considerada verdadeira
      - Se a OP não for atendida, pode ser devido a ela ser de fato falsa ou o modelo não ser 'inteligente' o suficiente para provar automaticamente.
        
        Uma verificação manual é necessária para garantir se está de fato provado ou não
      - Interactive Proof
        
        Conjunto de comandos gerados para tentar provar o que determinado trecho está tentando ser provado.
    - - As vezes as regras podem "quebrar" a prova em prova menores que são mais fáceis de entender/provar
        
        a : S <-> T é equivalente a provar que dom(a) : POW(S) e ran(a) : POW (t)
        
        qualquer intervalo de p..q é um subconjunto finito de INTEGER
        
        A U B = C é verdade se B U A = C é uma hipótese
        
        Quando todas as obrigações de provas são montadas, uma árvore de prova é gerada e, quando todas são provadas verdadeira, o trecho é provado verdadeiro
- - - - Durante uma prova interativa podemos executar uma série de comandos passo a passo para demonstrar que nossa suposição sobre o modelo é verdadeira
        
        Expressões que utilizamos podem ser simplificadas, decompostas e, ao final de cada passo, podem ser verificadas como verdadeiras ou não provadas. Caso todas sejam provadas a prova está finalizada.