Skip to content

Implementação do Tableux para Lógica Clássica de Primeira Ordem

Notifications You must be signed in to change notification settings

alexandrempierre/tableaux

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

10 Commits
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

tableaux

Implementação do Tableux para Lógica Clássica de Primeira Ordem.

Por questão de conforto em relação ao material e ao código que foi lido para escrever o programa, ele está em Inglês assim como toda a interação do programa com o usuário.

O arquivo a ser executado deve ser o main.py que já está pronto para execução por linha de comando no Linux (a menos de um chmod) (a main.py tem shebang).

Tecnologias utilizadas

Desenvolvido com:

  • Atom
  • Arch Linux
  • Tilix
  • Git
  • Github

Dependências:

  • Python 3.6.1

  • Biblioteca nltk

    O nltk foi escolhido pelo seu parser. Mas por mais completo que seja o parser do nltk, apenas uma parte dele vai ser usado. As únicas operações reconhecidas nesse programa são conjunção, disjunção, negação unária, implicação e os quantificadores existencial e universal. Essas operações podem ser feitas entre fórmulas, ou seja, podem aparecer umas dentro das outras (de uma forma um tanto específica). No código do programa não há menção a palavra "literal", optei por seguir o padrão e chamar de átomo negado ou n_atom no contexto.

    O parser do nltk reconhece outras operações como o "se e somente se", no caso de operações como essa o comportamento do Tableaux não está garantido, pois não foi feito tendo essa operação em mente, nem nenhuma outra que não tenha sido citada no parágrafo anterior.

Como utilizar

Após instalar o Python 3 e a biblioteca nltk, basta atribuir ao seu usuário a permissão de execução sobre o arquivo main.py e executá-lo.

$ chmod a+x main.py 	// permite que qualquer usuário execute o arquivo

Há duas formas possíveis de usar o tableaux:

  • Passando um arquivo (caminho relativo ou completo) como argumento de linha de comando para ao rodar o programa:

     $ ./main.py <nome do arquivo>
    
  • Passando os tableauxs a serem resolvidos para o programa durante sua execução

     $ ./main.py
    

    Nesse caso o programa tem textos de orientação ao usuário pedindo a informação necessária a cada passo. Esses textos foram escritos em Inglês.

Formato da Entrada

Para detalhes de como escrever as sentenças lógicas no nltk, a página mais direta que encontrei foi essa.

  1. número de tablôs a serem resolvidos
  2. Pergunta
  3. número de afirmações no BD
  4. BD (com um "Enter" ao final de cada afirmação do BD) (este passo se repete de acordo com o número digitado no passo 3)

As partes 2, 3 e 4 se repetirão de acordo com o valor digitado no passo 1.

Exemplo de entrada válida

2
A(a)
1
A(a)

exists x.A(x)
1
all x.A(x) | exists x.A(x)

About

Implementação do Tableux para Lógica Clássica de Primeira Ordem

Topics

Resources

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published

Languages