surfx / solver

Solver Tableau

Solver Tableau KE C# v1.0.0

Solver LCP (lógica clássica proposicional) de Tableau KE, versão 1.0.0

Solver em desenvolvimento, dúvidas, críticas, erros, sugestões são bem-vindas. O código é livre para uso, apenas peço a referência ao projeto.

Pode ser utilizado via linha de comando ou acesando diretamente as classes C#.

Libs necessárias: ver seção Libs

Exemplo de uso (linha comando)

Parâmetros aceitos

Parâmetro	Obrigatório	Tipo	Descrição
file_formulas	sim	entrada	arquivo onde estão as fórmulas lógicas
file_img	não	saída	arquivo onde a árvore de prova será salva
file_estatisticas	não	saída	arquivo onde as estatíticas serão salvas

Exemplo de uso:

$ dotnet run file_formulas=C:\Users\...\parser\formulas.txt file_img=C:\Users\...\parser\prova.png file_estatisticas=C:\...\Desktop\parser\estatisticas.txt

Ou:

$ cd ...\solver_project\project\solver\bin\Debug\net7.0\
$ .\solver.exe file_formulas=C:\Users\...\parser\formulas.txt file_img=C:\Users\...\parser\prova.png file_estatisticas=C:\...\Desktop\parser\estatisticas.txt

ps: novos parâmetros estão em desenvolvimento

Exemplo entrada file_formulas

O arquivo de entrada formulas.txt deve ter o seguinte formato:

T (A | C -> E) | (!C | B & E)
T !E
T B
F C & D
F !D
F !A

Exemplo saída file_estatisticas

O arquivo de saída estatisticas.txt para a entrada formulas.txt é:

Tempo: 18 ms, 00:00:00
Memória: [CPU=0, Allocated MemorySize=1.262.896, Survived = 483.920]
closed: True
Complexidade: 40
Bifurcacoes: 1
NumeroAtomosLivres: 10
NumeroFormulas: 16
RamosAbertosFechados: Abertos: 0, Fechados: 2
Alturas: min: 13, max: 13, avg: 1
NumeroConectores: 11
Contradições: 7 T A e 13 F A | 9 F E e 16 T E
RegraUnarias: (F ¬) 6 F ¬A: 7 T A | (F ¬) 3 F ¬D: 4 T D | (T ¬) 8 T ¬E: 9 F E
RegraBinarias: (F ˄2) 2 F C ˄ D, 4 T D: 10 F C | (T →2) 9 F E, 11 T (A ˅ C) → E: 12 F A ˅ C
RegraUnariaDouble: (F ˅) 12 F A ˅ C: 13 F A, 10 F C | (T ˄) 14 T (¬C ˅ B) ˄ E: 15 T ¬C ˅ B, 16 T E
RegraBeta: (T ˅) 1 T ((A ˅ C) → E) ˅ ((¬C ˅ B) ˄ E): 11 T (A ˅ C) → E, 14 T (¬C ˅ B) ˄ E

Exemplo saída file_img

Arquivo de saída prova.png para a entrada formulas.txt é:

Exemplo Parser (code C#)

Para referência direta, a sintaxa base é:

    Formulas f = new();

    Parser parser = new();
    f.addConjuntoFormula(parser.parserCF("A->B"));
    f.addConjuntoFormula(parser.parserCF("F C->E"));
    f.addConjuntoFormula(parser.parserCF("C"));
    f.addConjuntoFormula(parser.parserCF("F A"));
    f.addConjuntoFormula(parser.parserCF("T (A | D)"));

    f.addEsquerda(parser.parserCF("E"));
    f.addEsquerda(parser.parserCF("F Y -> (A | B)"));

    f.addDireita(parser.parserCF("T H->G"));
    f.addDireita(parser.parserCF("F (A|Z)"));
    f.addDireita(parser.parserCF("T G|T&U"));
    f.addDireita(parser.parserCF("T G|T&X"));
    f.Direita.addEsquerda(parser.parserCF("T G|T&U"));

    f.Esquerda.addDireita(parser.parserCF("G & (Y -> B)"));
    f.Esquerda.addDireita(parser.parserCF("F G"));

    f.Esquerda.addEsquerda(parser.parserCF("G & (Y -> B)"));

    f.Esquerda.Direita.isClosed = true;

Um exemplo de uso pode ser encontrado na classe classes.auxiliar.inputs.ExecucaoSolver.cs

Saídas

Formato string

Console.WriteLine(f.ToString());

obs: tags OPEN/CLOSED apenas ilustrativas

                                              1 T A
                                              2 T A → B
                                              3 F B
     4 F A → B                                                               11 F A ˅ B
     5 T C                                                                   12 T C ˅ A
6 T C              8 F ((C → B) ˄ C) ˅ D                                     13 T (C ˅ A) → B
7 F C         9 T A                     10 T B                               14 T C
OPEN          OPEN                      OPEN           15 T C
                                                       16 F C
                                                       17 F ((C → B) ˄ C) ˅ D
                                                       CLOSED

Imagem png

obs: tags OPEN/CLOSED apenas ilustrativas

    PFormulasToImage pf2img = PFormulasToImage.PFormulasToImageBuilder.Init(f)
            .SetPathImgSaida(string.Format(@"{0}\{1}", "imgformulas", "bmp_formula.png"))
            .withDivisoriaArvore()
            .Build();
    new ImageFormulas().formulasToImage(pf2img);

Estudos iniciais

Árvores				Parser

Regras Tableau KE

Exemplos de provas

Ainda não implementado. Imagens de exemplos retiradas do software KEMS e de material do professor doutor Adolfo Gustavo Serra Seca Neto, atualmente docente na UTFPR - Curitiba/PR.

Prova 1	Prova 2

TODO

• Estrutura de fórmulas - código C#, classes, etc
• Parser
• Print árvore string
• Print árvore png
• Stage, versão inicial (stage: conjunto de fórmulas)
• Separar a abstração do 'print árvore png' em uma classe parametrizada
• Regras binárias e unárias. Implementar Regras: F ˄1, F ˄2, T →1, T →2, T ˅1, T ˅2, F →, F ˅, T ˄, F ¬ e T ¬
• Regra PB (Princípio da bivalência)
• Regras beta: F ˄, T →, T ˅
• Aplicar conjunto de regras às fórmulas do stage
• Implementar o conceito de estratégia
• Verificar se os ramos estão abertos ou fechados
• Verificar se a árvore possui solução ou não
• Valoração / contra-exemplo
• Imprimir a árvore com o "número" da fórmula ao lado
• Melhorar o print toString()
• Validar árvore e métodos de prova com mais exemplos
• Implementar estratégia para escolha da regra beta a ser aplicada
• Criar estratégia para cálculo de complexidade e variabilidade das fórmulas do stage
• Log, tempo de execução, memória utilizada
• Análisar tempos de prova, altura da árvore, complexidade, etc
• Interface externa do console, para entradas e saídas
• Print tree dot mode

Libs

dotnet add package System.Drawing.Common --version 7.0.0

Obs

Para executar vscode: CTRL + F5 / F5 ou $ dotnet run

Urls

• Tableau KE proof
• símbolos alt
• Adolfo Gustavo Serra Seca Neto
• KEMS
• Consumo memória C#

Tutoriais Imagens

• Text on Image
• C# console write text image