KANREN is a declarative logic programming system with first-class relations, embedded in a pure functional subset of Scheme. The system has a set-theoretical semantics, true unions, fair scheduling, first-class relations, lexically-scoped logical variables, depth-first and iterative deepening strategies. The system achieves high performance and expressivity 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. KANREN works on any computer platform for which a Scheme implementation exists (from PalmPilot and iPAQ to Unix/Linux/Winxx/Mac workstations and servers to MindLego bricks). The system can be compiled or interpreted. Being essentially a Scheme library, KANREN can interact with the user through any graphical or command-line interface provided by the host Scheme implementation.
Keywords for this software
References in zbMATH (referenced in 5 articles )
Showing results 1 to 5 of 5.
- Tanter, Éric: Book review of: D. P. Friedman and C. Eatlund, The little prover (2020)
- Ahn, Ki Yung; Vezzosi, Andrea: Executable relational specifications of polymorphic type systems using Prolog (2016)
- Culpepper, Ryan; Felleisen, Matthias: Debugging hygienic macros (2010)
- Kiselyov, Oleg; Byrd, William E.; Friedman, Daniel P.; Shan, Chung-chieh: Pure, declarative, and constructive arithmetic relations. (Declarative pearl) (2008)
- Near, Joseph P.; Byrd, William E.; Friedman, Daniel P.: (\alpha)\textsflean\textitTAP: a declarative theorem prover for first-order classical logic (2008)