Kanren

Kanren is a declarative logic programming system with first-class relations embedded in a pure functional subset of Scheme. The system has true unions, fair scheduling, lexically-scoped logical variables, set-theoretical semantics, and high performance without cuts. Applications of the system range from expert systems to polymorphic type inference and overloading resolution, to model checking and theorem proving. The system can be used as a meta-logic system.