Implementation of Gentzen's Sequent Calculus (LK) applied to creating and interrogating a database in natural language
Roadmap:
- mathematical proof of well formation of the Prover (not possible: same as termination problem)
- translation from a subset of natural english to predicates (very complex, very hard subject, that's why we specify 'a subset')