eyekind guide

Give eyekind a few facts and rules, ask a question, and follow the answer back to its evidence. This guide takes you from a first conclusion to checked proofs, browser experiments, and your own Python application.

eyekind is a rule language written in Python. A program is a plain Python script, its conclusions, proofs and check reports are plain expressions, and the reasoner itself is a few thousand lines of Python that needs nothing beyond the standard library. One language states the rules, computes with them, and holds every result. The specification defines the language, what a run concludes, the proof format, and what proof checking establishes.

Start now: Try Socrates in the playground · Run locally · Check a proof

Contents

• Choose your starting point
• Install and run
• Your first program
  • Try a small change
• Writing programs
  • Deriving rules
  • Inspecting rules
  • Terms and names
  • RDF 1.2
• Reasoning strategy
• Proofs, and what checking one means
  • Why negation and collection are safe
• Checking the translation
• Explore the examples
• Browser
• CLI options
• Troubleshooting
• Python library
• What is deliberately absent
• Development and testing
  • Releases
• The name

Choose your starting point

Install and run

eyekind needs Python 3.9 or later and nothing else. From a checkout of the repository:

python -m eyekind examples/socrates.py

Your first conclusions are:

type('socrates', 'mortal')
type('socrates', 'human')

Open socrates.py beside its saved output. The program says Socrates is human and every human is mortal; a rule carries class membership to a superclass, and the query reports every class membership.

Now ask for the explanation, and check it:

python -m eyekind --proof examples/socrates.py > /tmp/socrates-proof.py
python -m eyekind --check-proof /tmp/socrates-proof.py examples/socrates.py

The report ends with verdict('checked'). You have run a program and checked a proof of its conclusions.

To have an eyekind command, run pip install eyekind, or pip install -e . in the checkout, which keeps using the checkout so your edits take effect at once. The commands below use eyekind; substitute python -m eyekind if you did not install it.

Your first program

Save this as /tmp/family.py, or paste it into the playground:

fact(parent('alice', 'bob'))
fact(parent('bob', 'carol'))

implies(parent(X, Y), ancestor(X, Y))
implies([ancestor(X, Y), parent(Y, Z)], ancestor(X, Z))

implied_by(related(X, Y), ancestor(X, Y))
implied_by(related(X, Y), ancestor(Y, X))

query(related('alice', 'carol'))

eyekind /tmp/family.py

prints related('alice', 'carol'). The two implies rules run forward: whenever their premise holds, they conclude their conclusion, until nothing new follows. The implied_by rules run backward, only when a goal asks for them. The two kinds compose: a forward rule may call backward definitions, and a backward goal may use the facts forward reasoning established, so you let knowledge accumulate and then ask a focused question.

With nothing asked, a run prints the facts it derived; query(...) asks the program’s own questions, and --goal asks from outside instead. The output opens with a comment saying which of these it holds, or that there is nothing to show, such as // Answers: each instance of a goal that holds.; reading the output back ignores comments:

eyekind --goal "ancestor('alice', Who)" /tmp/family.py

Try a small change

Add fact(parent('carol', 'dave')), run it again, and ask --goal "ancestor(X, 'dave')". Then remove a rule and see which answers disappear. The first unexpected answer is often worth the most, because it points at a specific rule or assumption to revisit.

Writing programs

A program states clauses with these calls:

A list is a conjunction. A premise is a goal or a list of goals that must all hold, and a forward rule’s conclusion may be a list of several conclusions: implies([p(X), q(X)], [r(X), s(X)]). Disjunction is or_(A, B), negation not_(G), alongside call, once and findall; and_(A, B) is a conjunction too. and, or, not and is are Python keywords, so a program spells them and_, or_, not_ and is_; the terms they build, and every document, spell them and(...), or(...), not(...) and is(...).

Deriving rules

Write a rule inside another rule’s conclusion with the same calls: implies(Body, Head) and implied_by(Head, Body). Lists work in both parts, and a conclusion can combine several templates and ordinary facts:

fact(enabled('demo'), p('a'), q('a'))
implies(enabled(Name), [
  implies([p(X), q(X)], [r(Name, X), s(Name, X)]),
  implied_by([known(Name, X), available(Name, X)], r(Name, X)),
])
query([known('demo', X), available('demo', X)])

The inner calls build templates; they do not also state standalone rules. An ordinary rule call still states a clause when its returned value is not embedded in another statement. Helpers can return rule values, and a stored value can be reused in several generators. Program builds collect these registrations independently. forward(Body, Head) and backward(Head, Body) are also available as pure template constructors.

This reports and(known('demo', 'a'), available('demo', 'a')). Name is captured from the generator. X appears only inside templates, so each template has its own local X, reused with fresh variables whenever its rule is applied. A variable shared with an ordinary sibling conclusion is also captured. A forward template’s head-only variables receive Skolem witnesses, including its captured context in their arguments.

Templates are compiled into guarded clauses before reasoning. A generator derives an activation; the generated rule requires that activation. Proofs show both clauses and the activation’s evidence, and the independent checker verifies them against the compiled source program. Activations are omitted from ordinary conclusions. All potential generated rules participate in stratification, so not_ and findall wait for their dependencies to finish, and closed dependency cycles are rejected. Their proof obligations remain visible as usual. Template bodies require statically named calls; a goal such as call(G) with variable G is rejected. Forward templates can nest; backward templates conclude ordinary heads.

See the decks for derived forward rules, derived backward rules, and a conjunction of backward templates. SPEC §6.2 defines the scope and lowering.

Inspecting rules

In a premise, the same calls inspect source rules as data:

fact(a('b'))
implies(a(X), c(X))
implies(implies(X, Y), test(X, Y))
query(test(X, Y))

The answer is test(a(A), c(A)): the inspected rule’s shared variable is preserved. The query selects that answer; forward reasoning also derives c('b'). implied_by(Head, Body) inspects backward rules. Inspection can match conjunctions or instantiate a pattern, and works in goals passed with --goal too. It examines structure without proving a rule’s premise.

The catalogue contains ordinary source rules. It excludes facts, queries, constraints, template generators, generated clauses, and rules with inspection goals, so an inspecting rule does not report itself. Write an inspection pattern in place: passing a stored rule value, as in r = implies(a(X), c(X)) and then implies(r, seen('yes')), embeds it, so that rule is no longer stated and the inspection finds nothing. Each match and each use of a derived pattern receives fresh variables. Its proof includes a source(N) step; the checker verifies the pattern against that source rule. Negation and collection still report their obligations, with the catalogue available to refute inconsistent evidence. If a conclusion introduces an existential witness, bind its inspected pattern variables first: a generic pattern cannot share one witness across all its instances.

See the rule inspection deck and SPEC §6.3.

Terms and names

Nothing to declare. A program is given the names it states clauses with: fact, implies, implied_by, forward, backward, query, contradiction, facts_from, struct, preds, vars, the controls and_, or_, not_, call, once, findall and fail, the primitives such as is_, unify and lt, and the library as eyekind. A name the program uses without defining it is a variable when it starts with a capital or an underscore, like X or _Rest, and a predicate otherwise, like parent. A program may start with from eyekind import *, which gives it the same names; it needs that line only to run as a script of its own, python program.py, which takes the same options as eyekind program.py.

Python’s builtins keep their meaning in ordinary Python code, so a program can compute with them. A builtin name used inside a statement, as type is in fact(type('socrates', 'human')), is a predicate instead, throughout the program, except for the builtins a program computes its clauses with: print, range, len, list, dict, set, tuple, str, enumerate, zip, sorted, reversed, isinstance, open, repr, chr, ord, iter, any, all, map and filter, and the builtins whose names start with a capital, such as Exception. A program that wants a predicate named like one of those says so: range_ = preds('range'). preds and vars take names separated by spaces or commas and give one predicate or variable, or a tuple of several, so a Python keyword can name one too: from_ = preds('from') builds from(...), and None_ = vars('None') is the variable None. A call of an undeclared predicate on its own, such as a misspelled fcat(p(1)), states nothing, so eyekind stops with an error instead of ignoring it.

Python computes the clauses. A program is a script, so loops, functions and constants work as usual; the deep taxonomy examples state a hundred thousand rules with a for loop:

for level in range(1, 11):
    implied_by(type(X, f'n{level}'), type(X, f'n{level - 1}'))

Once stated, a clause is a term, and reasoning over it calls no code of yours.

Terms are Python values. An atom is a string, 'socrates'; a list is a list, and [H, *T] has head H and tail T; a compound term is a call, parent('alice', 'bob'); and _ is a fresh variable at every occurrence. struct('hello world', X) builds a compound whose name is not an identifier.

Numbers are exact. Integers have no size limit, so the Fibonacci example computes F(10000), a 2,090-digit integer, exactly. A Python int is an integer and a Python float a float: 2 is the integer 2, and 2.0 and float(2) are the float 2.0. 1 and float(1) do not unify, yet compare exactly. Infinity and NaN are rejected, and a result that is not a finite real number stops the run rather than becoming a value.

unify, identical and compare answer different questions. The floats 0.0 and -0.0 unify and compare equal, but identical distinguishes their canonical texts, including inside lists and compounds. In a program, write them as 0.0 and -0.0; float(-0) is 0.0, because -0 is the integer 0.

Arithmetic is a term, not an operator. is_(Y, add(X, 1)) binds Y to X + 1, and gt(X, 1) compares. Operators do not apply to terms: X + 1 or X > 1 in a program stops it with a message that says what to write instead. Operators on plain numbers are Python’s own, so query(unify(Y, 3 + 4)) binds Y to 7. div is true division, floordiv and mod floor toward negative infinity, and round rounds half to even. The primitives (unify, is_, eq, lt and the other comparisons, type tests, functor, univ, atom_concat and the rest) are listed in SPEC §4, and the arithmetic functions in SPEC §5. Everything else, such as membership, mapping or graph traversal, is written as ordinary clauses.

Domains get representations, not syntax. eyekind has no built-in notion of RDF or of anything else: IRIs, typed literals, triples and quoted graphs are just terms, such as literal(V, lang(L)) or triple(S, P, O) (see RDF 1.2 below). A forward conclusion may contain variables its premise never binds, and then says that something exists. Each such unknown becomes a Skolem function of the activation: implies(person(X), has_parent(X, P)) concludes has_parent('ann', skolem(2, 'P', ['ann'])), the P of rule 2 for Ann.

Data that is not a program. Everything eyekind writes, conclusions, proofs and check reports, is a document: plain expressions, one per line. facts_from reads such a document as data and states each expression as a fact. It never executes the text, so it is also the safe way to take in data you do not trust; a data file written as a program would run as Python. It is what lets one run reason over another, as audited-grants reasons over its own check report:

facts_from('data.py')
facts_from(text=eyekind.check_report(result.proof_report))

RDF 1.2

RDF reaches eyekind as data, through rdf-interchange, whose converters turn Turtle, TriG, N-Triples or N-Quads into a document of rdf(Subject, Predicate, Object, Graph) terms for facts_from, and turn the rdf or result_rdf conclusions of a run back into N-Quads, Turtle or TriG. The terms are:

A rule matches inside a triple term by unification, and a statement about a triple is an ordinary quad: a reifier linked to a triple(S, P, O) by rdf:reifies. A literal’s value is text, so [atom_chars(Text, Chars), number_chars(N, Chars)] reads '98' as the integer 98, and the same two primitives in the other order write a computed number back as text. Something a rule says exists, a Skolem term, becomes a blank node labelled by that term, the same node for the same rule firing. The rdf12-* examples show triple terms, nesting, annotations, directional strings, typed numbers and named graphs.

Reasoning strategy

eyekind reasons in both directions within one run, and the statement chooses the direction:

The same knowledge can be stated either way. implies(human(X), mortal(X)) derives mortal('socrates') as soon as human('socrates') holds; implied_by(mortal(X), human(X)) decides it only when a goal asks mortal(Who). Forward rules suit closures and classifications, where every consequence is wanted: implies([path(X, Y), edge(Y, Z)], path(X, Z)) terminates on a cyclic graph because a fact already derived is not derived again. Backward rules suit computations driven by their inputs, such as arithmetic recursion or list processing, which forward chaining could not start without them. Backward chaining keeps no table of answers, so a backward rule that calls itself with the same goal recurses until a bound stops the run; such recursion belongs in a forward rule.

The two strategies work together. A goal is solved by a primitive or control when it is one, otherwise against the facts forward rules have derived, in the order derived, and then against the program’s facts and backward rules. So a forward rule’s premise can call a backward definition, such as gt(Score, 80) or a recursive count, and a backward rule can use facts forward rules derived. Goals given with --goal, or by a library call, are solved after forward reasoning has finished.

Forward rules run stratum by stratum. A negation or a findall is used only after every rule that could still produce what it inspects has reached its fixpoint (see Why negation and collection are safe). Within a stratum, rounds are evaluated semi-naively: a rule is searched again only for activations that use a fact derived since its last search, which concludes exactly what searching everything again would. A variable that appears only in a forward rule’s conclusion becomes a Skolem term of the activation, so a rule that says “something exists” names the same something however often it fires. max_depth, max_inferences and max_iterations bound a run, and exceeding one is an error, never a partial answer.

Two details make this fast without changing any result. Clauses are indexed on arguments that are atoms or numbers, so a goal such as type(X, 'n99999') goes straight to the clauses that can match. A clause used repeatedly is matched against a goal as a compiled pattern: its variables take the goal’s values directly, instead of being renamed and then unified.

When a proof is asked for, the first derivation of each conclusion is recorded, and the checker verifies that record against the program without calling the reasoner. SPEC §8 defines the search, the rounds, the Skolem terms and the bounds, and SPEC §6.1 the strata.

Proofs, and what checking one means

A proof holds the claims, the source clauses it cites, and one step(...) record per inference, each part introduced by a comment that says what it holds. The checker establishes eight conditions:

Two properties make this worth more than a log. The checker follows the certificate: it never calls the reasoner to fill a gap, so a missing step fails the check rather than being quietly re-derived. The source is the authority: the clauses a proof displays cannot override the program, so you cannot smuggle a rule into a proof, nor pad it with steps no claim needs. Every proof eyekind generates is checked before it is returned.

The report is a document too, so one program’s evidence is material another program can reason over:

// Checked answers: these follow from the input program.
type('socrates', 'mortal')
type('socrates', 'human')

// C1-C8: resolution, acyclicity, justification, coverage,
// re-decision, boundary consistency, relevance and witness integrity.
condition('C1', 'resolution', 'ok', 3)
condition('C2', 'well_founded', 'ok', 3)
condition('C3', 'justification', 'ok', 3)
condition('C4', 'coverage', 'ok', 4)
condition('C5', 're_decision', 'ok', 0)
condition('C6', 'boundary_consistency', 'ok', 0)
condition('C7', 'relevance', 'ok', 5)
condition('C8', 'witness_integrity', 'ok', 0)

// Proof statistics: recorded steps and how they were checked.
steps(3)
verified(3)
recomputed(0)
composed(0)
trusted(0)
claims(2)

// This verdict applies to the claims above; it does not establish completeness.
verdict('checked')

Use eyekind -c examples/socrates.py (or --prove-and-check) to generate a proof and check it against the input program in one command. --check-proof FILE checks a saved proof. Both outputs put the answers first, with comments explaining the checks and their verdict. Failed checks label the displayed claims as unverified; checks with obligations label the answers as conditional. JSON output includes an answers array.

Failures appear as failed(N) outcomes with failure(Condition, Conclusion, Detail) facts, an invalid proof gives verdict(failed(N)) and exit code 2, and --json gives the same report as JSON. Proofs are read as data and never executed, so checking a proof from someone else runs none of their code.

Why negation and collection are safe

A negation, not_(G), concludes something from what is not there, and a collection, findall(T, G, L), from everything that is there. Both are only right once nothing more can be derived. eyekind guards them in four ways.

Ask only once the answer is final. eyekind works out which clauses each body goal depends on, ranks the rules so that every rule that could still produce a fact a negation or collection inspects runs to its fixpoint first, and rejects a program with no such ranking:

implies(not_(q), p)
implies(p, q)     # p needs q to be absent, yet p yields q: rejected

Positive cycles, such as transitive closure, are fine. Ranks compare whole terms rather than predicate names, so t(X, 'type', Y) and t(X, 'status', Y) can sit at different ranks, which matters when everything is a triple.

Negate only what is bound. The variables of not_(G) must be bound when it is solved; otherwise eyekind stops with an error. When “no value at all” is what you mean, say so with _: not_(q(X, _)) holds when q(X, Y) has no solution for any Y.

Say what was taken on trust. A proof records each negation as an 'absent' step and each collection as a 'collected' step, the report lists them as obligation('absent', 'theory_scoped', Goal), and the verdict is checked_with_obligations. --strict-proof rejects any proof that leans on one.

Refute them when the evidence allows. An absence fails C6 when a fact of the program, a step of the proof or a recomputed primitive is a solution after all, and a collection fails when such a solution is missing from its list.

Checking the translation

A checked proof shows that the conclusions follow from the program. It cannot show that the program says what the law, the policy or the textbook says. What eyekind can do is point at the parts of a program that make no difference to its conclusions, because those are where a translation is most likely to be decorative, incomplete or untested:

fact(p('a'))
fact(q('b'))
implied_by(s(X), q(X))
fact(z('c'))
implies([p('a'), not_(s('a'))], 'ok')

$ eyekind --unused program.py
unused(line(2), fact(q('b')))
unused(line(3), implied_by(s(X), q(X)))
unused(line(4), fact(z('c')))

A clause is listed when no conclusion’s proof uses it. A negation or collection may consult a clause without its proof recording that search, as not_(s('a')) consults q('b'); for each such clause eyekind leaves it out, runs the program again, and lists it only when the conclusions stay the same.

Explore the examples

The example collection is 94 complete programs, each with its conclusions, proof and C1–C8 report saved beside it (examples/output/, examples/proof/, examples/check/), and a card deck that explains it for a wide audience. They range from classics (Ackermann, the zebra puzzle, Aunt Agatha) to practical planning (outage recovery, critical paths, battery dispatch), policy reasoning (research-portal, package-holiday), mathematical calculations (Bézout certificates, Pell equations, regression), RDF 1.2 data (the rdf12-* examples) and a hundred-thousand-level taxonomy. Change a fact, run it, and compare with the saved output to see exactly what your change did.

Browser

The playground runs eyekind’s own Python modules in your browser through Pyodide, in a worker, so a long run never freezes the page and Stop ends it; Python starts with the page and takes a few seconds. Each run is the eyekind command line, with the page’s inputs as its only files. Choose an example, load a program from a URL, or edit the program, pick an output (conclusions, --proof, --prove-and-check, --check-proof of a saved proof you paste or load, or --unused), optionally give a goal, reasoning bounds or --stats, and press Run or Ctrl+Enter. --strict-proof and --json are enabled only in the two checking modes. The options panel shows the equivalent eyekind command line, and Save output downloads what it printed. When an error names a line of the program, a syntax error included, that line is marked red in the input until you edit it. Inputs and options are saved in your browser.

Share link copies a link holding the program, the proof to check and the options; an unedited example with the default options gets a short #example=name link. Create Gist share uploads the same state to an unlisted GitHub Gist, with a GitHub token that has gist permission and stays in the tab, and copies a short link to it. To run the playground from a checkout, serve it, for example with python -m http.server, and open /playground/; browsers do not run workers from file://. The conformance page runs the conformance suite in the browser the same way, and opens a case’s program in the playground.

CLI options

eyekind [OPTION ...] [FILE ...]

Exit codes: 0 success, 1 error, 2 a proof that is not valid, 65 a contradiction.

Troubleshooting

Python library

from eyekind import check_proof, load_text, run

socrates = load_text("""
fact(human('socrates'))
implies(human(X), mortal(X))
""")
goals = ['mortal(X)']
result = run(socrates, goals=goals, proof=True)
print(result.answers)
print(result.bindings)
print(check_proof(socrates, result.proof, goals=goals)['valid'])

This prints ["mortal('socrates')"], [{'X': "'socrates'"}] and True. load_text(source, filename, io) loads program text and load_sources([(text, filename), ...], io) several sources as one program; pass host_io from eyekind.host as io to let facts_from(path) read files. build(function) makes a program from a function that states clauses when called; a function that takes one parameter is handed the program’s names, as in names.fact(...). run() returns a Result with answers, bindings, inferred, stdout, proof, proof_report, stats and halt_code; its options are goal, goals, proof, max_depth, max_iterations and max_inferences, and exceeding a bound raises an EyekindError rather than return a partial result. check_proof(program, document, goals=None, allow_trusted=True) checks a proof and returns its report as a dict, check_report(report) formats a report, and read_term, read_terms and write read and write the canonical text. A program reaches the same functions as eyekind.run, eyekind.build and so on.

Omit a reasoning bound or pass None to use its default. A supplied max_depth, max_iterations or max_inferences must be a positive safe integer; zero, fractions, strings and infinite values raise an EyekindError.

What is deliberately absent

Cut, conditional commitment, mutable databases, attributed variables, constraint libraries, tabling, and filesystem or network built-ins. Several of these omissions are load-bearing: without cut and without a mutable database, a derivation is a function of the program and its input, which is what makes a certificate meaningful. Undefined predicates fail, under the closed-world convention.

Development and testing

# ./test full suite, memory capped
systemd-run --user --scope -q -p MemoryMax=3G -p MemorySwapMax=0 -- ./test
# ./test only these sections
./test unit examples
# ./test only tests whose line contains "skolem"
./test -k skolem
# ./test only these examples
EYEKIND_EXAMPLES=socrates,graphs ./test examples
# ./test the playground in a headless Chrome
./test playground
# the playground tests alone, saving screenshots into DIR
python tests/browser.py DIR
# regenerate example artifacts after an intended change
python tools/update_examples.py
# run the conformance suite of SPEC.md
python conformance/run.py
# run the conformance suite of SPEC.md against another implementation
python conformance/run.py --command "my-eyekind"

The full suite and large examples need substantial memory. On this development machine, use the memory cap above with swap disabled and run one heavy job at a time. Focused tests can use ./test unit -k NAME; PYTHON chooses the interpreter ./test runs.

./test prints one numbered line per test, with what it tests and how long it took, and a total per section. The sections are the unit tests (tests/test_*.py), among them forged proofs the checker must reject, condition by condition; the example corpus, where each program must reproduce its saved output, proof and check report, its saved proof must check from scratch and strictly, a proof with an unjustified claim added must fail, and a separate named test for every check file verifies its answers and the one-command checking output; the conformance suite, run in process; and the same suite run through the eyekind command, one process per case. The last section is the playground, run in a headless Chrome at desktop and phone widths: examples load and run, proofs are made and checked in the page, errors mark their line, and a run is stopped. It needs Chrome or Chromium (google-chrome, chromium or chromium-browser on the PATH, or CHROME naming it) and Pyodide from its CDN, and says so and runs nothing when either is missing; python tests/browser.py DIR runs it alone and saves screenshots. python conformance/run.py --command "python -m eyekind" runs every case through the command too, and -v names each case as it passes. The conformance cases are generated by tools/sync_conformance.py from the shared suite of the specification and are not edited by hand; conformance/README.md describes the case format.

Review artifact changes together with the source change that caused them. When adding an example, register its name, description, expected halt code (if any) and proof obligations in examples/manifest.json, write its deck in examples/deck/, then generate its artifacts.

Releases

For maintainers, ./release (a patch release) or ./release minor "Release message" (or major) checks that the working tree is clean, pulls main, runs ./test, bumps the version in pyproject.toml and writes it into eyekind/__init__.py and SPEC.md with python tools/version.py --bump, commits, and pushes main and an annotated tag together. The message defaults to Release vX.Y.Z and becomes the commit, tag and release title. python tools/version.py writes the version of pyproject.toml into those files, and python tools/version.py --check fails when one of them disagrees.

The tag starts two workflows. .github/workflows/release.yml creates the GitHub release, which Zenodo archives through its GitHub integration. .github/workflows/publish-pypi.yml checks that the tag matches pyproject.toml, runs the tests, builds the package, and publishes it to PyPI. An existing release can be published again through Actions → Publish to PyPI → Run workflow, given its tag; the dry-run input builds the package without uploading it. A push to main runs CI (ci.yml: the tests on several Python versions, and the playground once, in Chrome) and deploys GitHub Pages (pages.yml).

PyPI publishing uses trusted publishing: the workflow exchanges its GitHub Actions identity for a short-lived token, so no PyPI token is stored. The project, eyekind, has its trusted publisher on pypi.org set to owner eyereasoner, repository eyekind, workflow publish-pypi.yml and environment pypi; renaming the repository, the workflow file or the environment requires updating that entry first.

The name

eyekind joins eye, after the EYE family of reasoners it belongs to, to kind: a reasoner of the EYE kind, whose conclusions come with reasoning that can be inspected and checked.