POPL 2025
Sun 19 - Sat 25 January 2025 Denver, Colorado, United States
Tue 21 Jan 2025 14:30 - 15:00 at Keep Away - Session 7 Chair(s): Daniela Inclezan

Dual Horn clauses mirror key properties of Horn clauses. We revisit Dual Horn clauses as enablers of a form of constructive negation that supports goal-driven forward reasoning and is valid both intuitionistically and classically. In particular, we explore the ability to falsify hypotheses in the context of a background theory expressed as a Dual Horn clause program.

With Dual Horn clause programs, by contrast to negation as failure, the variable bindings in their computed answers provide explanations for the reasons why a statement is successfully falsified.

We devise a compilation scheme from Dual Horn clause programs to Horn clause programs, ensuring their execution with no performance penalty and we design the embedded SymLP language to support combined Horn clause and Dual Horn clause programs.

As a (motivating) application, we cast LLM reasoning chains into propositional Horn and Dual Horn clauses that work together to constructively prove and disprove goals and enhance Generative AI with explainability of reasoning chains.

Tue 21 Jan

Displayed time zone: Mountain Time (US & Canada) change

14:00 - 15:30
Session 7PADL at Keep Away
Chair(s): Daniela Inclezan Miami University
14:00
30m
Talk
Exploring Answer Set Programming for Provenance Graph-Based Cyber Threat Detection: A Novel Approach
PADL
Fang Li Oklahoma Christian University, Fei Zuo University of Central Oklahoma, Gopal Gupta
14:30
30m
Talk
Leveraging LLM Reasoning with Dual Horn ProgramsRECORDED
PADL
Paul Tarau University of North Texas
15:00
30m
Talk
Enhancing network diagnosis with reflection in Prolog (extended abstract)RECORDED
PADL
Anduo Wang Temple University, USA
Pre-print