Thank you for sharing! A closely related puzzle was previously discussed at:

https://news.ycombinator.com/item?id=14400017

The present puzzle can be seen as a natural continuation of this earlier thread, and the declarative programming language Prolog is again well-suited for this puzzle.

For example, we can start with a short Prolog program that exhaustively generates all solutions:

    numbers_tree([N], leaf(N)).
    numbers_tree(Vs0, binary(Left, Right)) :-
            permutation(Vs0, Vs),
            append([L|Ls], [R|Rs], Vs),
            numbers_tree([L|Ls], Left),
            numbers_tree([R|Rs], Right).

    tree_op_expr_value(leaf(N), _, number(N), N).
    tree_op_expr_value(binary(Left0, Right0), Op, expr(Op,Left,Right), Value) :-
            tree_op_expr_value(Left0, _, Left, VL),
            tree_op_expr_value(Right0, _, Right, VR),
            op_values_value(Op, VL, VR, Value).

    op_values_value(+, A, B, V) :- V is A + B.
    op_values_value(-, A, B, V) :- V is A - B.
    op_values_value(×, A, B, V) :- V is A * B.
    op_values_value(÷, A, B, V) :- B =\= 0, V is A rdiv B.

We can query it like this:

    ?- numbers_tree([4,6,6,6], T),
       tree_op_expr_value(T, _, Expr, 24).

On backtracking, it generates all solutions, reported as abstract syntax trees Expr.

This is of course not yet the full task. And I won't solve the full task here, because I would like to give others a chance to also have a look. However, I post a hint towards an efficient solution:

In such cases where you want to detect whether something is "essentially the same", consider applying a notion from term rewriting: In term rewriting, we apply rewrite rules, and in strongly normalizing systems, each term has a so-called normal form, which is its canonical representation.

Thus, in the language of term rewriting, when trying to decide if two terms are "essentially the same", you can reduce both of them to their respective normal forms, and then compare the normal forms! The two original terms are the same iff their normal forms are the same.

Here is part of the term rewriting system I have come up with for this task, implemented in Prolog:

    commutative(+).
    commutative(×).

    expr_normal_form(number(N), number(N)).
    expr_normal_form(expr(Op,A0,B0), expr(Op,A,B)) :-
            commutative(Op),
            expr_comparison(A0, B0, Comp),
            smaller_first(Comp, A0, B0, A, B).
    expr_normal_form(expr(Op,A0,B0), expr(Op,A,B)) :-
            \+ commutative(Op),
            expr_normal_form(A0, A),
            expr_normal_form(B0, B).

    smaller_first(=, A0, B0, A, B) :-
            expr_normal_form(A0, A),
            expr_normal_form(B0, B).
    smaller_first(<, A0, B0, A, B) :- smaller_first(=, A0, B0, A, B).
    smaller_first(>, A0, B0, A, B) :- smaller_first(<, B0, A0, A, B).

    expr_comparison(number(A), number(B), C) :- compare(C, A, B).
    expr_comparison(number(_), expr(_,_,_), <).
    expr_comparison(expr(_,_,_), number(_), >).
    expr_comparison(Expr, Expr, =).
    expr_comparison(expr(Op1, _, _), expr(Op2, _, _), C) :-
            dif(Op1, Op2),
            compare(C, Op1, Op2).
    expr_comparison(expr(Op,A0,B), expr(Op,A,B), C) :-
            dif(A0, A),
            expr_comparison(A0, A, C).
    expr_comparison(expr(Op,A,B0), expr(Op,A,B), C) :-
            dif(B0, B),
            expr_comparison(B0, B, C).

It works by imposing an order on terms, and recursively rewriting a single term to its normal form, which is smaller than or equal to the original term according to that (self-imposed) order.

We can now use an additional predicate like the following to collect all solutions, remove duplicates, then rewrite each solution to its respective normal form, and then remove duplicates again:

    all_expressions(Ls, Value, Exprs) :-
            findall(Expr, (numbers_tree(Ls, T),
                           tree_op_expr_value(T, _, Expr, Value)), Exprs0),
            sort(Exprs0, Exprs1),
            maplist(expr_normal_form, Exprs1, Exprs2),
            sort(Exprs2, Exprs).

For example, in the [4,6,7,9] = 24 case, this algorithm reduces the expressions to 5 solutions:

    ?- all_expressions([4,6,7,9], 24, Exprs),
       maplist(portray_clause, Exprs),
       length(Exprs, L).
    expr(×, number(6), expr(÷, expr(+, number(7), number(9)), number(4))).
    expr(×, expr(+, number(7), number(9)), expr(÷, number(6), number(4))).
    expr(÷, number(6), expr(÷, number(4), expr(+, number(7), number(9)))).
    expr(÷, expr(+, number(7), number(9)), expr(÷, number(4), number(6))).
    expr(÷, expr(×, number(6), expr(+, number(7), number(9))), number(4)).
    Exprs = [...],
    L = 5 .

I leave adding more rewrite rules as a challenge.