Knowledge bases and queries¶

A logic program is a theory: facts stating what is true, and rules stating what is true provided that their body is. A solver answers queries against a theory, enumerating every solution by backtracking.

See also: Your first logic program, Query solvers.

In [1]:

from tuprolog.solve.prolog import prolog_solver
from tuprolog.theory.parsing import parse_theory

family = parse_theory("""
    parent(abe, homer).    parent(mona, homer).
    parent(homer, bart).   parent(marge, bart).
    parent(homer, lisa).   parent(marge, lisa).

    grandparent(X, Z) :- parent(X, Y), parent(Y, Z).
    ancestor(X, Y) :- parent(X, Y).
    ancestor(X, Y) :- parent(X, Z), ancestor(Z, Y).
""")
solver = prolog_solver(static_kb=family)
len(family)

from tuprolog.solve.prolog import prolog_solver from tuprolog.theory.parsing import parse_theory family = parse_theory(""" parent(abe, homer). parent(mona, homer). parent(homer, bart). parent(marge, bart). parent(homer, lisa). parent(marge, lisa). grandparent(X, Z) :- parent(X, Y), parent(Y, Z). ancestor(X, Y) :- parent(X, Y). ancestor(X, Y) :- parent(X, Z), ancestor(Z, Y). """) solver = prolog_solver(static_kb=family) len(family)

Out[1]:

9

query yields the bindings of each solution as a dictionary of Python values:

In [2]:

list(solver.query("grandparent(G, lisa)"))

list(solver.query("grandparent(G, lisa)"))

Out[2]:

[{'G': 'abe'}, {'G': 'mona'}]

In [3]:

for answer in solver.query("ancestor(abe, D)"):
    print(answer["D"])

for answer in solver.query("ancestor(abe, D)"): print(answer["D"])

homer
bart
lisa

solve_once returns the first Solution, which is truthy if the query succeeded:

In [4]:

yes = solver.solve_once("parent(P, bart)")
no = solver.solve_once("parent(bart, _)")
bool(yes), yes["P"], bool(no)

yes = solver.solve_once("parent(P, bart)") no = solver.solve_once("parent(bart, _)") bool(yes), yes["P"], bool(no)

Out[4]:

(True, homer, False)

Solutions are computed lazily, so infinite ones can be explored too; limit caps their number:

In [5]:

naturals = prolog_solver(static_kb=parse_theory("nat(0). nat(s(N)) :- nat(N)."))
list(naturals.query("nat(N)", limit=4))

naturals = prolog_solver(static_kb=parse_theory("nat(0). nat(s(N)) :- nat(N).")) list(naturals.query("nat(N)", limit=4))

Out[5]:

[{'N': 0}, {'N': s(0)}, {'N': s(s(0))}, {'N': s(s(s(0)))}]

Changing the knowledge base¶

Clauses in the static knowledge base cannot change; those in the dynamic one are added and removed by assertz/1 and retract/1, e.g. to keep state:

In [6]:

counter = prolog_solver(dynamic_kb=parse_theory("count(0)."))
for _ in range(3):
    counter.solve_once("retract(count(N)), M is N + 1, assertz(count(M))")
list(counter.query("count(N)"))

counter = prolog_solver(dynamic_kb=parse_theory("count(0).")) for _ in range(3): counter.solve_once("retract(count(N)), M is N + 1, assertz(count(M))") list(counter.query("count(N)"))

Out[6]:

[{'N': 3}]

Built-in predicates¶

Solvers come with Prolog's standard built-ins: arithmetic, term inspection, all-solutions predicates, control constructs, and more.

In [7]:

list(solver.query("findall(C, parent(homer, C), Children), atom_length(homer, L), X is 2 ** 10"))

list(solver.query("findall(C, parent(homer, C), Children), atom_length(homer, L), X is 2 ** 10"))

Out[7]:

[{'Children': ['bart', 'lisa'], 'L': 5, 'X': 1024.0}]

In [8]:

list(solver.query("member(X, [a, b, c]), X \\== b"))

list(solver.query("member(X, [a, b, c]), X \\== b"))

Out[8]:

[{'X': 'a'}, {'X': 'c'}]