Most programming feels like giving detailed instructions to a very literal assistant. This is imperative programming — you tell the computer exactly how to solve your problem.

Declarative programming is about stating what you want rather than how to do it. The difference between turn-by-turn directions versus stating your destination and letting GPS choose the route.

The Magic of Stating Rules Instead of Steps

In declarative languages like Prolog, you don’t write algorithms. You write facts and relationships:

1
2
3
4

parent(john, mary).
parent(mary, alice).
ancestor(X, Y) :- parent(X, Y).
ancestor(X, Y) :- parent(X, Z), ancestor(Z, Y).

The system doesn’t execute a predefined sequence — it tries to prove your question is true based on the rules you’ve given it.

Proof Trees: Maps of All Possible Reasoning

It constructs a proof tree — a structure showing how a query can be proven from facts and rules. Each node is a goal, each child is a subgoal generated by applying a rule, and a successful proof is a path from root to leaves (facts).

1
2
3
4
5
6

ancestor(john, alice)
├── Try Rule 1: Is john a direct parent of alice? ❌
└── Try Rule 2: Is there someone between them?
    └── Find: parent(john, mary) ✓
        └── Now prove: ancestor(mary, alice)
            └── Check: parent(mary, alice) ✓

Proof Engines: Automated Explorers

The proof engine walks this tree. It takes your question, finds applicable rules, breaks big questions into smaller subquestions, explores each possibility systematically, backtracks when it hits dead ends, and keeps searching until it finds a complete proof.

You never tell it how to search. You just provide the logical structure, and it figures out the exploration strategy.

Why This Changes Everything

Imperative: You control the how — every step is explicit Declarative: You define the what — the system generates the how

The implications are profound: less code (describe relationships once), more flexible (same rules answer many questions), self-optimising (engine chooses efficient search strategies), naturally recursive (complex hierarchies emerge from simple rules).

The Foundation

This proof-tree approach isn’t limited to Prolog. SQL databases build query execution plans as trees. CSS selectors match DOM elements through rule cascades. Constraint solvers explore solution spaces systematically.

What makes these systems “declarative” is this separation: you describe the what (rules, constraints, goals), and the engine handles the how (search, optimisation, execution).

Behind every declarative query is an invisible tree of possibilities, and proof engines are the explorers that traverse them.