CoTaVeRa - Construtor de Tabelas-Verdade e Ramificações |
|
Versão 3.1 (c) Ricardo Pereira Tassinari
|
Está página faz tabelas-verdades e ramificações (tableaux) para fórmulas e (condicionais associadas a)
argumentos da Lógica Proposicional Clássica e da Lógica Clássica de Primeira Ordem.
Para inserir um símbolo da tabela abaixo, basta inserir, com um espaço antes e um depois, a palavra entre parênteses que o segue.
| Notação |
| Conectivos Negação ~ (-) Conjunção ⋀ (e) Disjunção inclusiva ⋁ (ou) Disjunção exclusiva ẇ (ouou) Condicional → (imp) Bicondicional ↔ (sss) |
| Quantificadores Universal ∀ (pt) Existencial ∃ (ex) |
| Constantes Individuais Pode-se usar qualquer seqüência de letras. |
| Variáveis Individuais Pode-se usar qualquer letra, desde que seu quantificador esteja explícito (se não, é tratada como constante). |
| Símbolos de Predicados Pode-se usar qualquer seqüência de letras. |
| Símbolos de Funções Não são permitidos. |
| Símbolos Auxiliares Parêntese Esquerdo ( Vírgula , Parêntese Direito ) |
| Símbolo de Dedução ⊦ (deduz) |
| Observações Não é necessário colocar parênteses externos nas fórmulas. O programa faz tabelas-verdade de fórmulas de 1ª ordem sem quantificadores. |
| Exemplos (clique no exemplo para o copiar no campo de fórmulas) ~(A⋀B)→((B⋁A)↔(AẇB)) ~(Mortal(Sócrates)⋀~Mortal(Sócrates)) ∀xP(x)→∃yP(y) Grego(Sócrates) , ∀x(Grego(x)→Mortal(x)) ⊦ Mortal(Sócrates) |