package datalog

  1. Overview
  2. Docs

Main Datalog module

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.


Universal type

module Univ : sig ... end

This module is present to allow the user to extend explanations with her own types.

Main module type

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

Signature for a symbol type

module type SymbolType = sig ... end

A symbol must be hashable, comparable and printable.

Hashconsing of symbols

module Hashcons (S : SymbolType) : sig ... end

Main functor

module Make (Symbol : SymbolType) : S with type symbol = Symbol.t

Build a Datalog module. This allows to specialize Datalog for a user-defined type of atoms. Strings are a good default, but more complicated types can be useful.