
1. instalacao:
	use o comando: make all


2. Modo de uso:
	provador [parametros]
	
	
3. parametros reconhecidos:
	-t		: roda a bateria de testes.
	-o<arquivo>	: imprime no arquivo selecionado os resultados de
			performance das frmulas calculadas.
			Caso no seja definido um arquivo de sada, no sero
			gerados os resultados de performance.
	-f<arquivo>	: l o arquivo selecionado e executa os comandos encontrados
	-v<frmula>	: verifica se a frmula dada  satisfatvel. Imprime uma
	                resposta em caso positivo.
	-v<sequente>	: verifica se o sequente  uma tautologia.
	-n<0-9>		: define o grau de 'silencio' da execuo do programa, onde 0
			indica nenhuma reduo no nmero de mensagens geradas na sada
			padro e 9 significa reduo total de mensagens.
	-m<0-1>		: atualmente o programa pode rodar com o algoritmo trivial ou
			com uma ligeira otimizao. Para rodar o programa com o 
			algoritmo trivial utilise 0, para rodar com a otimizao
			utilise 1. O padro  o algoritmo trivial.

observao:
	os parmetros so avaliados da esquerda para a direita e executados
	imediatamente.

4. comandos do Makefile:
	- all		: recompila todos os arquivos de cdigo fonte pendentes.
	- rebuild	: recompila todos os arquivos de cdigo fonte.
	- clean		: apaga todos os arquivos objeto e o executavel criados.

5. formato do arquivo de entrada:
	Cada comando pode se estender por mais de uma linha.
	Cada comando deve ter os caracteres "\>" no incio de sua primeira linha.
	Todas as linhas antes do primeiro comando so descartadas.
	No  possvel colocar comentrios entre cada comando.


6. linguagem reconhecida:
sequente	: premissas |- concluso
premissas	: frmula | premissas,frmula
frmula		: identificador | (frmula)And conjuno | Not(frmula) |
		  (frmula)Or disjuno | (frmula)->(frmula) | Box(frmula)

conjuno	: (frmula) | (frmula)And conjuno

disjuno	: (frmula) | (frmula)Or disjuno


identificador	: sequncia de letras e/ou dgitos (o primeiro caractere deve
		  ser uma letra). Ateno ao usar 'And', 'Or' ou 'Not' como
		  identificadores.
				
observao: brancos no alteram a identificao da frmula, a menos em um
	identificador de varivel.

7. exeplos de uso:
	provador -t
		roda a bateria de testes

	provador -v(ax)And(by)
		verifica a frmula (ax)And(by)

	provador "-v ((ax) And (by)) -> (( Not(bx) ) Or (ay))"
		verifica a frmula ((ax)And(by))->((Not(bx))Or(ay))

	provador -t -v"(m)->(n)" -vNot(t)
		roda a bateria de testes, verifica a frmula (m)->(n) e
		verifica a frmula Not(t)

	provador -n2 -m1 -fBateriaDeTestes -oresultados
		define o nvel de silencio de execuo para 2, determina que
		seja usado o algoritmo alternativo para o clculo de frmulas
		lgicas, processa o arquivo chamado "BateriaDeTestes", por fim
		define que os prximos resultados obtidos sejam impressos no
		arquivo de nome "resultados" (observe que esta atribuio
		ocorre aps o arquivo de testes ser processado, portanto os
		resultados deste no aparecem no arquivo de resultados).


