Can LLM Aid in Solving Constraints with Inductive Definitions?

Weizhi Feng, Shidong Shen, Jiaxiang Liu +3

Solving constraints involving inductive (aka recursive) definitions is challenging. State-of-the-art SMT/CHC solvers and first-order logic provers provide only limited support for…