s(CASP)

Top-down, non-monotonic, backward chaining reasoner for evaluating Constraint Answer Set Programs. No grounding - can execute programs that are not finitely groundable!

Very odd procedural semantics. Non-Herbrand universe, "constructive" negation based on dual rules

Builds on s(ASP) by adding constraints.

Literature

best practices guide. Has advice on aggregation, which is fiddly
about justifications

Uses

Original implementation in Ciao, also implemented in SWI-Prolog by Wielemaker
Jason Morris is a fan. s(CASP) is open source and explainable, and Morris has implemented defeasibility (I think) and some interesting relevance filtering.
Blawx is backed by s(CASP), L4 can compile to s(CASP), and a piece of Singapore legislation (Rule 34) has been encoded in s(CASP).