Extending logic programming beyond the first-order paradigm has long been a chal- lenge due to the complexity of handling higher-order constructs and negation. This the- sis investigates the evaluation of second-order Datalog with negation, which extends the expressiveness of traditional logic programming while maintaining declarative seman- tics. Prior research introduced a three-valued immediate consequence operator to com- pute the well-founded model for higher-order programs, yet the computational overhead of this approach limits its scalability.
We propose a bottom-up evaluation framework that combines program transforma- tion techniques with alternating fixpoint evaluation to systematically refine approxima- tions of the well-founded model. This approach introduces a new way to handle nega- tion in second-order logic programs and presents an alternative framework for evaluat- ing the well-founded semantics. It contributes to a deeper understanding of higher-order logic programming and its potential use in complex reasoning tasks.