  Dual Horn clauses mirror key properties of Horn clauses. This paper explores
the ``other side of the looking glass'' to reveal some expected and unexpected
symmetries and their practical uses.
  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 a counterfactual hypothesis 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. Moreover, in the
propositional case, by contrast to negation as failure as implemented with
stable models semantics in ASP systems, and similarly to Horn clause programs,
Dual Horn clause programs have polynomial complexity.
  After specifying their execution model with a metainterpreter, 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.
