Parse Problems

[adolfont]

Example

A sequent such as p, p->q |- q

[adolfont]

Some links related to parsing https://www.one-tab.com/page/SiXgf2HSR32oDVhUDvbhbA

[adolfont]

Maybe use NimbleParsec https://stefan.lapers.be/posts/elixir-writing-an-expression-parser-with-nimble-parsec/

[luissimas]

We'll be dealing with signed formulas in the tableaux, but the input string will be a sequent containing unsigned formulas right?

So given the input: p, p->q |- q the parser could produce something like:

[
  %{formula: :p, sign: :T},
  %{formula: {:implies, :p, :q}, sign: :T},
  %{formula: :q, sign: :F}
]

And those would be the formulas in the root of the proof tree

[adolfont]

Exactly, @luissimas. The the input string will be a sequent containing unsigned formulas and a "|-" sign.

Your example is quite good.