ELPI & higher-order reasoning.

A logic program states facts and rules. A query asks the engine to find substitutions that make a goal follow. The program describes a relation rather than prescribing every step of an algorithm.

% A tiny λProlog relation
kind animal type.
type tom animal.
pred cat o:animal.
pred mammal o:animal.
cat tom.
mammal X :- cat X.

With the query mammal X, the engine can discover X = tom. This is a successful search relative to this program. The declaration and clause spelling should be run with the project’s documented command-line or Lean integration.

Search and verification are different responsibilities. A printed answer is not, by itself, a Lean theorem. If you need certification, select a path that records derivations and connects them to a checker.

Try it

If the search does not find another mammal, have you proved that none exists?

Higher-order representations can make functions and predicates part of the data being manipulated. For syntax containing bound variables, higher-order abstract syntax uses the logic language’s binding machinery to represent object-language binding.

% A typing rule for an object-language lambda
of (lam F) (arr A B) :-
  pi x\ of x A => of (F x) B.

This fragment comes from the kind of simply typed lambda-calculus example developed in LeanElpi’s introduction. Read it as follows: introduce a fresh x; assume locally that x has type A; under that assumption, show that F x has type B.

The pi binder and hypothetical implication => make scope explicit. The temporary assumption is used inside the goal. It is not a permanent write to an agent’s database.

Try it

Why should a hypothetical question not silently update the shared knowledge graph?

A useful architecture gives the search component freedom to change while keeping the acceptance rule small and explicit.

1. State the goal. Identify the graph snapshot, formal vocabulary, and exact query.
2. Search. Let Elpi construct a derivation using admissible rules.
3. Record evidence. Export a proof object or certificate with the dependencies needed to replay the reasoning.
4. Check. Verify each step and connect successful checking to the goal through a soundness theorem.

LeanElpi’s optional LF layer and LeanRDF’s certificate checker are two concrete parts of this ecosystem. They have different formats and interfaces; choose the mechanism appropriate to your claim.

Be precise about execution. A verified checker has a theorem about its behavior. A compiled program running that checker also depends on runtime machinery. Constructing a Lean theorem using native computation has its own trust assumptions. Inspect the actual route used by the project rather than treating all three as interchangeable.

Try it

A certificate is syntactically valid but references a premise absent from the input graph. Should it be accepted?