A parser for first-order logic reasoning.
The main purpose in developing a first-order logic reasoner involves the modelling of a learning tool, aiming to cover some contents of classical Artificial Intelligence related to the Logic studies. The resolution by tableau method is one of such topics which helps to understand the concepts behind the logical reasoning. To achieve such tool, a parser is needed to analyse the logical expressions and it should be able to interpretate semantically the sentences along the reasoning process.
FOLParser was developed in Java using the ANTLR 4.0 framework (https://www.antlr.org/). The semantic layer uses the tableau method for resolution. At the moment, this version is working fine with propositional logic and some aspects of FOL, requiring improvements for both universal and existential quantifiers. Some kind of sentences with quantifiers were tested, giving correct results. A test case with 18 propositional formulas was implemented in JUnit, printing in console the formal reasoning using the tableau method. A graph of each resolution by tableau is generated using dot (Graphviz).
Some representation definitions:
- Variables starting with underline (e.g. _A, _B, etc)
- Predicate symbols (e.g. _P(#a), _Q(#b), with constants #a, #b, etc)
- Functions (e.g. _F(?x), _G(?y), with variables ?x, ?y, etc)
- Logic operations use the commonplace symbols (AND as &, OR as |, NOT as ~).
- Logical implication (->)
- Logical equivalence (<->)
- Quantifiers (FORALL and EXISTS)
A FOL endpoint using the parser is available here.
1.01 - 16/11/2021
Printing of sentences and resolution by tableaux in LaTex is also available.
(_A | _B) -> _B
1: (_A|_B)->_B = false (F)
2: (_A|_B) = true (F)
3: _B = false (T)
4: _A = true (T)
4: _B = true (T)
LaTex:
The generated graph for this resolution is:
((_A -> _Q(#b)) & ~_Q(#b)) -> ~_A
1: ((_A->_Q(#b))&~_Q(#b))->~_A = false (F)
2: ((_A->_Q(#b))&~_Q(#b)) = true (F)
3: ~_A = false (F)
4: (_A->_Q(#b)) = true (F)
5: ~_Q(#b) = true (F)
6: _A = false (T)
7: _Q(#b) = false (T)
8: _A = true (T)
6: _Q(#b) = true (T)
7: _Q(#b) = false (T)
8: _A = true (T)
FORALL(?x)(_F(?x)->_G(?x)) -> _F(#a)
1: FORALL(?x)(_F(?x)->_G(?x))->_F(#a) = false (F)
2: FORALL(?x)(_F(?x)->_G(?x)) = true (F)
3: _F(#a) = false (T)
4: _F(?x)->_G(?x) = true (F)
5: _F(?x) = false (T)
5: _G(?x) = true (T)
FORALL(?x)(_A(?x) & _B(?x)) -> (FORALL(?x)(_A(?x)) & FORALL(?x)(_B(?x)))
1: FORALL(?x)(_A(?x)&_B(?x))->(FORALL(?x)(_A(?x))&FORALL(?x)(_B(?x))) = false (F)
2: FORALL(?x)(_A(?x)&_B(?x)) = true (F)
3: (FORALL(?x)(_A(?x))&FORALL(?x)(_B(?x))) = false (F)
4: _A(?x)&_B(?x) = true (F)
5: _A(?x) = true (T)
6: _B(?x) = true (T)
7: FORALL(?x)(_A(?x)) = false (F)
8: _A(?x) = false (T)
7: FORALL(?x)(_B(?x)) = false (F)
8: _B(?x) = false (T)
EXISTS(?y)(FORALL(?x)(_R(?x?y))) -> FORALL(?x)(EXISTS(?y)(_R(?x?y)))
1: EXISTS(?y)(FORALL(?x)(_R(?x?y)))->FORALL(?x)(EXISTS(?y)(_R(?x?y))) = false (F)
2: EXISTS(?y)(FORALL(?x)(_R(?x?y))) = true (F)
3: FORALL(?x)(EXISTS(?y)(_R(?x?y))) = false (F)
4: FORALL(?x)(_R(?x?y)) = true (F)
5: _R(?x?y) = true (T)
6: EXISTS(?y)(_R(?x?y)) = false (F)
7: _R(?x?y) = false (T)
Obs.: Test cases were based on the sentences of Mortari's book (2001), exercise 12.1.
PARR, T. The Definitive ANTLR 4 Reference. Dallas, Texas: The Pragmatic Programmers, LLC, 2012.
RUSSELL, S.; NORVIG, P. Inteligência Artificial (Artificial Intelligence). R. de Janeiro: Elsevier, 2004.
(Author: Luciano F. de Medeiros)