Owl is a tiny logic programming language highly inspired by prolog.
Installing simply requires dune.
git clone https://github.com/jdrprod/owl.git
cd owl
dune install owl
The syntax of Owl is very similar to prolog. We can define facts and rules:
A Fact
likes(foo, bar).
Notice that capital case characters are not allowed
A Rule
likes(?x, meat) :- carnivores(?x).
Notice that variables are introduced using a question mark
This rule could be expressed in first order logic as forall x, carnivores(x) -> likes(x, meat)
.
We can express logical operators by using the symbols &
or |
:
green(?x) :- blue(?x) & yellow(?x).
colored(?x) :- red(?x) | yellow(?x) | blue(?x).
Disjunctions can also be expressed by repeating several times a rule and modifying its right-hand side:
colored(?x) :- red(?x).
colored(?x) :- yellow(?x).
colored(?x) :- blue(?x).
Owl comes with a special notation for natural numbers. They are defined in the style of Peano : a natural number is simply zero or the successor of an other natural number. The successor function is abbreviated s
and the constant z
denotes zero. We can then represent 3 as s(s(s(z)))
in Owl. To prevent writing unreadable programs, we can also use the standard notations 1, 2, 3 ...
. Owl will automatically convert numbers into the internal representation.
Facts and rules should be defined inside a text file. The file can then be loaded using the command owl path/to/file
. This will start an interactive session allowing to type queries.
Here is a simple implementation of natural numbers addition :
sum(z, ?x, ?x).
sum(s(?x), ?y, s(?z)) :- sum(?x, ?y, ?z).
The following query computes the sum of 1 and 1 :
sum(1, 1, ?x).
-> sum(1, 1, 2)
We can also define data-structures such as lists in Owl :
list(nil).
list(cons(?head, ?tail)) :- list(?tail).
Here is a simple implementation of append
. This implementation takes the form of a predicate defined recursively.
list_append(nil, ?x, cons(?x, nil)).
list_append(cs(?head, ?tail), ?x, cs(?head, ?next)) :- list_append(?tail, ?x ?next).
To compute the result of appending an element to a list, we can type the following query :
?- list_append(cons(1, cons(2, cons(3, nil))), 4, ?x)
-> list_append(cons(1, cons(2, cons(3, nil))), 4, cons(1, cons(2, cons(3, cons(4, nil)))))
The beauty of logic programming is that we can also ask what parameters give a specific result :
?- list_append(cons(1, ?x), ?y, cons(1, cons(2, cons(3, nil))))
-> list_append(cons(1, cons(2, nil)), 3, cons(1, cons(2, cons(3, nil))))
The complete example including sorting functions is available in the examples directory.
The current implementation of the solver behind Owl is not guarantee to terminate against any query. Nevertheless, some recent modifications have been done to reduce this limitation. There is work in progress to improve the solver and make it both powerful and reliable. In some cases, rewriting rules by changing the order of the conjuncts may prevent the solver to be trapped in infinite loops.