Provador para método de resolução

Provador feito na matéria de programação lógica com intuito de automatizar provas por resolução. Estratégia para resolver o problema de resolução foi busca por profundidade.

Operação Aceitas No Momento

• ~ é a negação
• v é o OR
• & é o AND
• => é a implicação

Como utilizar o provador

• Baixar swi-prolog em sua máquina. Download Prolog
• Carregar o arquivo no terminal do prolog com

  [provador_cabral].

• Testar exemplos

  solve(((p => q) => p) => p).
  solve(p v (~(q & (r => q)))).
  solve(q => ( p => r) & ~r & q => ~p).

Os Resultados do Teste devem ser o seguintes