Building a Mini Prolog Engine in Python - With Arithmetic Constraints
So far, I have been arguing in favor of logic programming as a powerful tool for symbolic reasoning and AI agents. I’ve shown how to use pip install pyswip to use Prolog, but we can actually embed it.
We will implement a simple Prolog interpreter in this post. The best working version can be found in my kb-agents repo.
Prolog in a nut shell
A prolog program is made of clauses, which can be either facts or rules. A fact is always true; a rule has a head and a body, and it states that if the body is true, then the head is also true. A query is a list of goals we want to prove using the facts and rules in the knowledge base (KB).
We can model graphs easily in Prolog:
edge(a, b).
edge(b, c).
path(X, Y) :- edge(X, Y).
path(X, Y) :- edge(X, Z), path(Z, Y).
This small program packs a full graph traversal engine. The edge/2 predicate defines the edges of the graph, and the path/2 predicate defines how to find paths using those edges.
A query to check if there is a path from a to c and to query all nodes that have a path to c would look like this:
?- path(a, c).
yes.
?- path(X, c).
X = b ;
X = a ;
no.
Business Rules in Prolog
This if-then-else style of programming is very expressive for business rules. Consider that a car rental agent should only offer a car if the user has a budget greater than the car’s price and has a driving license. This can be expressed in Prolog as:
offer_car(User, Car) :-
budget(User, Budget),
price(Car, Price),
Budget > Price,
has_driving_license(User).
If you read my earlier posts, you saw that we can model an agent via an action/1 predicate that resolves to a term that the LLM can understand.
We would start with a schema for the knowledge base:
:- dynamic budget/1.
:- dynamic has_driving_license/0.
:- dynamic intent/1.
:- dynamic customer_likes/1.
:- dynamic car/4.
And add facts such as:
car(car1, toyota, 2020, 30000).
car(car2, ford, 2019, 25000).
car(car3, honda, 2021, 28000).
We can add cars to the inventory simply by asserting any of car_price/2, car_model/2, car_brand/2, or car_year/2. This allows us to work with partial information about cars.
Now we use auxiliary predicates to model the business rules:
customer_qualified :-
budget(Budget),
has_driving_license,
intent(rent_car),
customer_likes(Car).
customer_affords(Car) :-
price(Car, Price),
budget(Budget),
Budget > Price.
can_offer(Car, Brand, Year, Price) :-
customer_qualified,
customer_affords(Car),
car(Car, Brand, Year, Price).
If we call can_offer(Car, Brand, Year, Price), what happens?
First it tries to prove customer_qualified/0. It will try to find a fact saying so in the database or find a rule that matches it. It looks for the rule, finds it, and this creates new goals: finding a solution for budget(Budget). Since it fails.
Now assume there is indeed a fact budget(30000). It finds it, and the goal is satisfied. It moves to the next goal, has_driving_license/0. If it is present as a fact, it is satisfied. Then it moves to intent(rent_car), which is also satisfied if present as a fact. Finally, it moves to customer_likes(Car). This is a predicate with a variable, so it looks for any fact that matches it. If there is a fact like customer_likes(car1), it finds it and the goal is satisfied.
Next comes checking if the customer can afford the car. It looks for the price(Car, Price) predicate. If there is a fact like price(car1, 28000), it finds it and binds Price to 28000. Then it looks for budget(Budget) again, which is already known to be 30000. Finally, it checks if 30000 > 28000, which is true, so the goal is satisfied.
Having satisfied both customer_qualified/0 and customer_affords(Car), it moves to the final goal, which is to find a car that matches the car(Car, Brand, Year, Price) predicate. It looks for any fact that matches this pattern. If there is a fact like car(car1, toyota, 2020, 30000), it finds it and binds Car to car1, Brand to toyota, Year to 2020, and Price to 30000.
In general, to answer a query:
We find a rule that matches it;
Find values for variables in the rule that make the rule true;
If the rule has a body, we recursively try to prove each predicate in the body;
If we reach a point where all predicates are satisfied, we have found a solution (a substitution for the variables in the query);
As we go through the goals, we keep a list of arithmetic constraints that must be satisfied for the solution to be valid; we check these constraints at the end.
This is called SLD resolution (Selective Linear Definite clause resolution) with arithmetic constraints.
As a second example, here is a Prolog program that defines family relationships and ages, and includes an arithmetic constraint to find all grandchildren older than 5 years:
parent(alice, bob).
parent(bob, carol).
grandparent(X, Y) :- parent(X, Z), parent(Z, Y).
age(alice, 50).
age(bob, 30).
age(carol, 10).
age(ike, 5).
?- grandparent(alice, Y), age(Y, Age), Age >= 6.
This is what knowledge representation looks like. But how do we build an engine that can process this?
Step 1: AST representation for Prolog
The prolog grammar maps directly to a simple AST.
class Term:
pass
@dataclass
class Const(Term):
name: str
def __hash__(self):
return hash(self.name)
def is_numeric(self) -> bool:
try:
float(self.name)
return True
except ValueError:
return False
def numeric_value(self) -> float:
return float(self.name)
@dataclass
class Var(Term):
name: str
def __hash__(self):
return hash(self.name)
@dataclass
class Predicate(Term):
name: str
args: list[Term]
def is_arithmetic_constraint(self) -> bool:
return (
self.name in {”=”, “!=”, “<”, “<=”, “>”, “>=”, “+”, “*”, “-”, “/”, “mod”}
and len(self.args) == 2
)
@dataclass
class Rule:
head: Predicate
body: list[Predicate]
Step 2: Adding Arithmetic Constraints
For arithmetic constraints, we need to defined a way to represent them and evaluate them. We will store new constraints as we progress through the goals, and check them at the end. This means we must always ground a integer constant in order to solve; we are not doing symbolic algebra here.
@dataclass
class ArithmeticConstraint:
op: Literal[”=”, “!=”, “<”, “<=”, “>”, “>=”, “+”, “\*”, “-”, “/”, “mod”]
left: Term
right: Term
def evaluate(self, subst: “Subst”) -> bool:
left_eval = subst.apply(self.left)
right_eval = subst.apply(self.right)
if isinstance(left_eval, Const) and isinstance(right_eval, Const):
if not left_eval.is_numeric() or not right_eval.is_numeric():
return False
left_value = left_eval.numeric_value()
right_value = right_eval.numeric_value()
match self.op:
case “=”:
return abs(left_value - right_value) < 1e-6
case “!=”:
return left_value != right_value
case “<”:
return left_value < right_value
case “<=”:
return left_value <= right_value
case “>”:
return left_value > right_value
case “>=”:
return left_value >= right_value
case _:
return False
return False
@dataclass
class ConstraintStore:
constraints: list[ArithmeticConstraint]
def add_constraint(self, constraint: ArithmeticConstraint):
self.constraints.append(constraint)
def is_satisfied(self, subst: “Subst”) -> bool:
return all(constraint.evaluate(subst) for constraint in self.constraints)
Step 3: Keeping Track of Substitutions and the Knowledge Base
We need to keep track of substitutions during unification and resolution. A substitution is a mapping from variables to terms. Since our queries contain variables, what we really want is to find substitutions that make the query true.
@dataclass
class Subst:
mapping: dict[Var, Term]
def apply(self, term: Term) -> Term:
if isinstance(term, Var) and term in self.mapping:
return self.apply(self.mapping[term])
elif isinstance(term, Predicate):
return Predicate(term.name, [self.apply(arg) for arg in term.args])
else:
return term
def extend(self, var: Var, term: Term):
self.mapping[var] = term
The knowledge base is simply a list of rules. When we begin to resolve a goal, we need to find all rules whose head predicate matches the goal predicate. This is a simple name and arity match.
@dataclass
class KB:
rules: list[Rule]
def get_rules_for_predicate(self, predicate: Predicate) -> list[Rule]:
return [
rule
for rule in self.rules
if same_name(rule.head, predicate) and same_arity(rule.head, predicate)
]
Step 4: Unification and SLD Resolution
The unification algorithm is the core of Prolog. First, we apply the current substitution to both terms. Then, we check the structure of the terms:
If one is a variable, we extend the substitution.
If both are constants, they must be equal.
If both are predicates, we recursively unify their arguments.
(Note how the match statement requires Python 3.10+, but enables very clean pattern matching and case analysis.)
def unify(x: Term, y: Term, s: Subst | None) -> Subst | None:
if s is None:
return None
x = s.apply(x)
y = s.apply(y)
match (x, y):
case Var() as v, _:
if v != y:
s.extend(v, y)
return s
case _, Var() as v:
return unify(v, x, s)
case Const() as c1, Const() as c2:
if c1.name == c2.name:
return s
else:
return None
case Predicate() as p1, Predicate() as p2:
if not same_name(p1, p2) or not same_arity(p1, p2):
return None
return unify_list(p1.args, p2.args, s)
case _:
return None
The main SLD resolution algorithm. SLD works by taking a goal, finding a rule that matches the goal, unifying the goal with the rule’s head, and then replacing the goal with the rule’s body (after applying the substitution). When this process results in an empty list of goals, we have found a solution. We use recursion to explore all possible resolutions.
def sld_resolution(
kb: KB,
goals: list[Predicate],
subst: Subst | None = None,
counter: int = 0,
constraints: ConstraintStore | None = None,
) -> list[tuple[Subst, ConstraintStore]]:
if subst is None:
return []
if constraints is None:
constraints = ConstraintStore([])
if not goals:
if constraints.is_satisfied(subst):
return [(subst, constraints)]
else:
return []
first, *rest = goals
solutions: list[tuple[Subst, ConstraintStore]] = []
# Check if the first goal is an arithmetic constraint
constraint = predicate_to_constraint(first)
# If a constraint, extend the store.
if constraint:
new_constraints = ConstraintStore(constraints.constraints + [constraint])
solutions.extend(sld_resolution(kb, rest, subst, counter, new_constraints))
# Else, proceed regularly.
else:
for rule in kb.get_rules_for_predicate(first):
renamed_head, new_counter = rename_vars(rule.head, counter)
new_subst = unify(first, renamed_head, Subst(subst.mapping.copy()))
if new_subst is not None:
# Ugly type checking hack...
new_goals = [subst.apply(g) for g in rule.body + rest]
solutions.extend(sld_resolution(kb, new_goals, new_subst, new_counter))
return solutions
And that’s it. Did you think it would take a tad more than a hundred lines of code?
Example usage
if __name__ == “__main__”:
kb = KB(
rules=[
Rule(
head=Predicate(”parent”, [Const(”alice”), Const(”bob”)]),
body=[],
),
Rule(
head=Predicate(”parent”, [Const(”bob”), Const(”carol”)]),
body=[],
),
Rule(
head=Predicate(”parent”, [Const(”bob”), Const(”ike”)]),
body=[],
),
Rule(
head=Predicate(”grandparent”, [Var(”X”), Var(”Y”)]),
body=[
Predicate(”parent”, [Var(”X”), Var(”Z”)]),
Predicate(”parent”, [Var(”Z”), Var(”Y”)]),
],
),
Rule(
head=Predicate(”age”, [Const(”alice”), Const(”50”)]),
body=[],
),
Rule(
head=Predicate(”age”, [Const(”bob”), Const(”30”)]),
body=[],
),
Rule(
head=Predicate(”age”, [Const(”carol”), Const(”10”)]),
body=[],
),
Rule(
head=Predicate(”age”, [Const(”ike”), Const(”5”)]),
body=[],
),
]
)
query = [
Predicate(”grandparent”, [Const(”alice”), Var(”Y”)]),
Predicate(”age”, [Var(”Y”), Var(”Age”)]),
Predicate(”>=”, [Var(”Age”), Const(”6”)]),
]
results = sld_resolution(kb, query, Subst({}))
query_vars = {Var(”Y”)}
for result, cs in results:
print(cs.constraints)
print(
{var.name: result.apply(var) for var in result.mapping if var in query_vars}
)
Conclusion
In about 150 lines, we’ve built a working Prolog-in-Python engine supporting:
Logical inference via SLD resolution
Variable binding via unification
Arithmetic constraints via a constraint store
This small engine can serve as:
A core reasoning engine for symbolic AI
A teaching tool for logic programming
A backend for hybrid LLM + logic agents
And this is much simpler than using PySwip/SWI Prolog, and safer, since:
It runs sandboxed in process, without external dependencies
It is pure Python, so it can be easily inspected and modified
It has no support for I/O operations, so it is safe to run untrusted code
Appendix
This is a helper function to convert a predicate to an arithmetic constraint if applicable.
def predicate_to_constraint(predicate: Predicate) -> ArithmeticConstraint | None:
if predicate.is_arithmetic_constraint():
return ArithmeticConstraint(
predicate.name, predicate.args[0], predicate.args[1]
)
return None
As we apply rules, we need to rename their variables, so that they don’t clash with variables in other rules or the query. We do this by appending a counter to the variable names. This is a simple way to ensure uniqueness.
def rename_vars(predicate: Predicate, counter: int) -> tuple[Predicate, int]:
new_args: list[Term] = []
for arg in predicate.args:
if isinstance(arg, Var):
new_args.append(Var(f”{arg.name}_{counter}”))
counter += 1
else:
new_args.append(arg)
return Predicate(predicate.name, new_args), counter
For unifying lists of terms, we can use a fold operation.
def unify_list(xs: list[Term], ys: list[Term], s: Subst | None) -> Subst | None:
if s is None:
return None
if len(xs) != len(ys):
return None
for x, y in zip(xs, ys):
s = unify(x, y, s)
if s is None:
return None
return s
And the helper functions to check predicate name and arity.
def same_name(x: Term, y: Term) -> bool:
return isinstance(x, Predicate) \
and isinstance(y, Predicate) and x.name == y.name
def same_arity(x: Term, y: Term) -> bool:
return isinstance(x, Predicate) \
and isinstance(y, Predicate) and len(x.args) == len(y.args)