Leveraging LLM Reasoning with Dual Horn Programs

Explore a conference talk from the 27th International Symposium on Practical Aspects of Declarative Languages that examines how Dual Horn clauses can enhance large language model reasoning capabilities. Discover how these clauses enable constructive negation supporting goal-driven forward reasoning that is valid both intuitionistically and classically. Learn about their ability to falsify hypotheses within a background theory and how, unlike negation as failure, they provide explanations through variable bindings for why statements are successfully falsified. The presentation covers a compilation scheme from Dual Horn clause programs to Horn clause programs that ensures execution without performance penalties, and introduces the embedded SymLP language supporting combined Horn and Dual Horn clause programs. See how LLM reasoning chains can be cast into propositional Horn and Dual Horn clauses to constructively prove and disprove goals, ultimately enhancing Generative AI with explainable reasoning chains. Presented by Paul Tarau from the University of North Texas at PADL 2025, sponsored by ACM SIGPLAN.