Construir um verificador de prova para o método axiomático.
Dada uma prova no sistema axiomático, ele verifica se a prova proposta está construída de forma correta, ou seja, se todas as instâncias de axiomas e uso do modus ponens foram usados de forma correta.
- símbolos atômicos: a,b,c,....,w,y,x,z. (letras do alfabeto em minúsculo);
- conectivos binários: & (conjunção), v (disjunção), > (implicação);
- conectivo unário: ¬ (negação);
- símbolos auxiliares: ),( - parênteses
- Todas as proposições atômicas são fórmulas;
- Se A e B são fórmulas então (A&B), (AvB), (A>B) também são fórmulas;
- Se A é fórmula então (¬A) também é fórmula;
- Toda fórmula só pode ser obtida por 1,2 e 3.
Prova Correta:
1 (a>((a>a)>a)) A1 p=a;q=(a>a)
2 ((a>((a>a)>a)) > ((a>(a>a))>(a>a))) A2 p=a;q=a;r=a
3 ((a>(a>a))>(a>a)) MP 1,2
4 (a>(a>a)) A1 p=a;q=a
5 (a>a) MP 3,4
A prova acima está correta pois todas as instâncias de axiomas foram utilizadas de forma correta, assim como o modus ponens.
Prova Incorreta:
1 (a>((a>a)>a)) A1 p=a;q=(a>a)
2 ((a>((a>a)>a)) > ((a>(a>a))>(a>a))) A2 p=a;q=a;r=a
5 ((a>(a>a))>(a>a)) MP 1,2
6 (a>(a>a)) A1 p=a;q=a
7 (a>a) MP 5,6
A prova acima está errada pois a numeração não está correta (as linhas 3 e 4 foram suprimidas).
Será necessário alterar as informações contidas no arquivo entrada.txt seguindo o padrão de 'numerolinha axioma numeroAxioma subisituições' ou 'numerolinha axioma ModusPoneis' (exemplo: '1 (a>((a>a)>a)) A1 p=a;q=(a>a)'), sendo que cada linha do arquivo só pode conter axioma ou modus ponens.
Após isso deve executar o comando python code.py no terminal, para ver o resultado do programa.