module BottomUp:sig
..end
Datalog is a fragment of first-order logic. It can be viewed as relational algebra with deduction/recursion (through Horn clauses).
A Datalog database contains facts and clauses (or rules). A fact
is simply a relational atom, like mother(mary, john)
. A Horn clause
is a deduction rule, for instance grandmother(X,Y) :- mother(X,Z), parent(Z,Y)
and parent(X,Y) :- mother(X,Y)
.
The Datalog_cli
module provides a simple client that demonstrates most
of the features of Datalog. Some basic examples can be found in the
tests/ directory.
module Univ:sig
..end
This module is present to allow the user to extend explanations with her own types.
Main module, that exposes datatypes for logic literals and clauses, functions to manipulate them, and functions to compute the fixpoint of a set of clauses
module type S =sig
..end
module type SymbolType =sig
..end
A symbol must be hashable, comparable and printable.
module Hashcons:
module Make:
Build a Datalog module.