Algorithm for parsing first order logic formulas

Question

I am trying to write an algorithm for converting formulas in first order (predicate) logic to abstract syntax trees. For propositional logic, I used the shunting-yard algorithm, but it does not work out of the box for first order logic since parenthesis may be used either in grouping or specifying the scope of predicates (or functions). Is there a generalization of the shunting-yard algorithm that can deal with this particular complication?

For reference, the strings I'm trying to parse look something like this:

"AxEy(P(x) & R(x,y)) -> R(f(a),b)"

Answer 1

An open parenthesis is a predicate scope or function argument list delimiter if and only if it immediately follows a predicate or function, respectively. If it is used for grouping, it must following a prefix or infix operator or another open parenthesis.

It doesn't really matter if you can't a priori identify function names, as long as they must have names; a parenthesis following a name is either a predicate scope or an argument list delimiter. It would be helpful to be able to identify predicates, of course.

You need to mark the parenthesis when you push it onto the stack so that you can create the correct AST node when you later pop it with its corresponding close parenthesis. If it's a predicate scope grouper or an argument list grouper, you need to include the predicate/function as part of the AST; it will be just underneath the open parenthesis on the stack.