Is it a valid number theory expression?

Question

A number theory expression contains:

There exists at least one non-negative integer (written as E, existential quantifier)
All non-negative integers (written as A, universal quantifier)
+ (addition)
* (multiplication)
= (equality)
>, < (comparison operators)
&(and), |(or), !(not)
(, ) (for grouping)
variable names(all lowercase letters and numbers, not necessary one char long)

However, it has some more limitations:

• Arithmetic expressions should be syntactically valid. Here we only treat + as addition, not positive, so + and * should be surrounded by two number expressions
• brackets should be well paired
• < = > should be surrounded by two number expressions
• & | ! are fed with logical expressions
• E and A are fed with a variable and an expression
• For E and A, there should be a reasonable affected range. (*)

For (*): We write Ax Ey y>x & y=x, Ax Ey y>x & Ey y=x as well as Ax Ey y>x & Ax Ey y=x, which mean Ax (Ey ((y>x) & (y=x))), Ax ((Ey (y>x)) & (Ey (y=x))) and (Ax (Ey (y>x))) & (Ax (Ey (y=x))); however we don't write Ax Ey Ax x=y or Ax Ey x<y & Ex x>y. That means there should be some way to add brackets, so everywhere any variable is at most defined for once, and anywhere that use the variable has it defined.

Input

You'll be given an expression with these chars (invalid chars won't appear), only split when necessary (two variable names together), split after each quantifier variable, or each symbols are separated. No invalid symbol.

Output

Check whether it's a valid number theory expression. Either true/false or multi/one are allowed.

True samples (each symbol separated)

E a E b a < b
E b A x b < x & A x b > x
E b A x b < x & b > x
A b b + b < ( b + b ) * b | E x x < b
E x E y y < x & E x2 y = x2
E 1 A x x * 1 = x & E 2 2 * 2 = 2 + 2 & 2 > 1 & E x x + 1 = x * x * 2
E x E y y = y & y + y * y = y

False samples

E a E b a + b < c
E a E b b * ( a > a ) + b
A a A b ( a = b ) = b
A x A y A z A y x < z
E x E y y < x & E x y = x
E E x x = x
E x ( x < x
E x = x

Undefined behavior samples

E C C = C
AA x x = x
Ex = x

Shortest code in bytes win

Symbol definition: It's a resexpr

numexpr({s},∅) = s
numexpr(a∪b,c∪d) = numexpr(a,c) + numexpr(b,d)
numexpr(a∪b,c∪d) = numexpr(a,c) * numexpr(b,d)
numexpr(a,c) = ( numexpr(a,c) )
boolexpr(a∪b,c∪d) = numexpr(a,c) = numexpr(b,d)
boolexpr(a∪b,c∪d) = numexpr(a,c) < numexpr(b,d)
boolexpr(a∪b,c∪d) = numexpr(a,c) > numexpr(b,d)
boolexpr(a∪b,c∪d) = boolexpr(a,c) & boolexpr(b,d)
boolexpr(a∪b,c∪d) = boolexpr(a,c) | boolexpr(b,d)
boolexpr(a,c) = ! boolexpr(a,c)
boolexpr(a,c) = ( boolexpr(a,c) )
boolexpr(a-{s},c∪{s}) = E s boolexpr(a,c) if s∉c
boolexpr(a-{s},c∪{s}) = A s boolexpr(a,c) if s∉c
resexpr = boolexpr(∅,a)
a,b,c,d mean sets, s mean non-empty strings containing a-z0-9

Notes

• You don't need to check whether the expression is true, as it's usually impossible

Answer 1

APL (Dyalog Unicode), ^{318 317} 319 bytes^SBCS

∨/{(4=⊃⍵)>≢⊃1⌽⍵}¨{1=≢⍵:⍵⋄⊃,/(⊂⍵)∇{⊃,/,(⍺⍺⍵↑⍺)∘.{c←⊃¨⍺⍵⋄w←⊃,/⊃¨u v←1↓¨⍺⍵
(⊂c)∊t←↓10 2⍴⎕A⍳'AOBAJACKANEADMLDJDGK':⊂(2,u)(1w 0)(3,v)(1u 0)(5(⊃u)⍬)(4w⍬)(6,u)(4,v)(7,v)(4,u)⊃⍨t⍳⊂c
6 4≡c:⊂4,u,¨v
9 1≡c:(2⊃v)↑⊂8,v
8 4≡c:(a∊3⊃⍵)↓⊂4(a~⍨⊃v)((3⊃⍵),a←⊃u)
⍬}⍺⍺⍵↓⍺}¨⍳¯1+≢⍵}{⌈/c←(⊃⍵)∊¨¯1⌽'()!',↓4 3⍴' &|=<>+* AE':8+⊃⍸c⋄1(⊂⍵)1}¨' '(≠⊆⊢)⍞

Try it online!

^{-1 byte thanks to @Adám.}

^{+2 bytes because the code wrongly accepted E ( a ) a = a. Fixed by adding a "simple" flag to the Num node, which is 1 right after tokenization but becomes 0 after any kind of merging. TQuant Num -> Quant rule is accepted only if "simple" is 1.}

Full program. Takes a line of input (each symbol separated with a space) from stdin, and prints 1 if it can be parsed successfully, 0 otherwise.

How it works: the grammar & parsing

I manually dissected all the grammar rules into two-branch rules, e.g. the parenthesizing rule

"(" Num ")" -> Num

became two rules

"(" Num -> NumP
NumP ")" -> Num

with NumP being a new node type. Also, I omitted the last part of the Num node, as it is always an empty set.

(Num ids,?) [+*] -> (NumR ids)
(NumR ids) (Num ids2,?) -> (Num (ids+ids2),0)
"(" (Num ids,?) -> (NumP ids)
(NumP ids) ")" -> (Num ids,0)
(Num ids,?) [=<>] -> (BoolN ids,[])
(BoolN ids,ids3) (Num ids2,?) -> (Bool (ids+ids2),ids3)
(Bool ids,ids2) [&|] -> (BoolR ids,ids2)
(BoolR ids,ids3) (Bool ids2,ids4) -> (Bool (ids+ids2),(ids3+ids4))
"!" (Bool ids,ids2) -> (Bool ids,ids2)
"(" (Bool ids,ids2) -> (BoolP ids,ids2)
(BoolP ids,ids2) ")" -> (Bool ids,ids2)
[EA] (Num id,1) -> (Quant id)
(Quant id) (Bool ids,ids2) -> (Bool (ids-id),(ids2+id)) if id not in ids2

Using these rules, I could tackle the ambiguous parsing problem as follows:

1. Split the given list of tokens into two chunks.
2. Recursively get all possible parses for the two chunks.
3. Test all combinations of parses to gather all possible derived parses.
4. Repeat 1-3 for all possible splits, and gather all results.

The algorithm is exponential in the number of tokens, so the two longest test cases are excluded from the tests.

Original version with comments

⍝ Constants to classify the grammar node type
Num NumR NumP Bool BoolN BoolR BoolP Quant TQuant TParenL TParenR TNot TBool2 TCmp TNum2←⍳15

⍝ Split given string by spaces, and convert to a list of grammar nodes
tokenize←{
  words←(' '∘≠⊆⊢)⍵  ⍝ split by spaces
  {
    class←(⊃⍵)∊¨'AE' '(' ')' '!' '&|' '=<>' '+*'
    ⌈/class: 8+⊃⍸class  ⍝ Single-char tokens into respective nodes
    Num(⊂⍵)1  ⍝ An identifier is a Num node
  }¨words  ⍝ wrap each word into tokens
}

⍝ Takes two nodes, and gives a new node if valid, ⍬ otherwise
match←{
  class←⊃¨⍺⍵
  Num TNum2≡class: ⊂NumR(2⊃⍺)
  NumR Num≡class: ⊂Num((2⊃⍺),2⊃⍵)0
  TParenL Num≡class: ⊂NumP(2⊃⍵)
  NumP TParenR≡class: ⊂Num(2⊃⍺)0
  Num TCmp≡class: ⊂BoolN(2⊃⍺)⍬
  BoolN Num≡class: ⊂Bool((2⊃⍺),2⊃⍵)⍬
  Bool TBool2≡class: ⊂BoolR(2⊃⍺)(3⊃⍺)
  BoolR Bool≡class: ⊂Bool((2⊃⍺),2⊃⍵)((3⊃⍺),3⊃⍵)
  TNot Bool≡class: ⊂Bool(2⊃⍵)(3⊃⍵)
  TParenL Bool≡class: ⊂BoolP(2⊃⍵)(3⊃⍵)
  BoolP TParenR≡class: ⊂Bool(2⊃⍺)(3⊃⍺)
  ⍝ Valid only if "simple" flag of Num node is 1
  TQuant Num≡class: (3⊃⍵)↑⊂Quant(2⊃⍵)
  ⍝ Valid only if quantified variable is not already quantified
  Quant Bool≡class: (~(2⊃⍺)∊3⊃⍵)↑⊂Bool((2⊃⍵)~2⊃⍺)((3⊃⍵),2⊃⍺)
  ⍬
}

⍝ Given a list of tokens, returns an array of possible parses
⍝ Split in all possible ways and check for at least one split is valid
parse←{
  ⍝ Single token: no need to parse
  1=≢⍵:⍵
  splits←⍳¯1+≢⍵
  ⍝ Concatenate parses based on all possible splits
  ⊃,/(⊂⍵)∇{
    left←⍺⍺ ⍵↑⍺
    right←⍺⍺ ⍵↓⍺
    ⍝ Test all possible combinations of left/right parses
    ⊃,/,left ∘.match right
  }¨splits
}

⍝ Test if one of the parses is Bool with no free variables
test←{
  ∨/{
    Bool≠⊃⍵:0
    0=≢2⊃⍵
  }¨⍵
}

⍝ The solution is the chain of three functions defined above
test∘parse∘tokenize

Try it online!