SEE - Symbolic Explanation Engine

SEE is a small rule engine for Prolog-style Horn clauses over ordinary terms, lists, arithmetic, strings, and finite search. The command-line executable is see.

Programs write relations directly, for example ancestor(pat, emma) or status(case1, accepted). SEE output is ordinary SEE syntax: each answer fact is followed by a why/2 explanation that records the proof. When no --query is supplied, the CLI materializes distinct new binary derivations of the form p(S, O), suppresses repeated source facts, and prints each derived answer with its explanation. Programs may add materialize(Name, Arity). declarations to focus default output on selected predicates.

Try it in the browser playground. The playground includes run options equivalent to CLI --query and --stats.

For the normative language definition, including lexical syntax, terms, clauses, goals, built-ins, memoize/2, materialize/2, and conformance boundaries, read SPEC.md.

Contents

1. Quick start
2. Running SEE
3. Default output
4. Writing programs
5. Aggregation helpers
6. Formula data
7. Example catalog
8. Golden outputs, tests, and conformance
9. Development and release
10. Performance notes
11. Implementation limits

Quick start

Install dependencies, if any, and run the command-line executable:

npm install

There is no build step for the CLI. Run examples, explicit queries, multiple inputs, stdin, or a URL:

bin/see --version
bin/see examples/ancestor.pl
bin/see --query 'ancestor(pat, X)' examples/ancestor.pl
bin/see facts.pl rules.pl
printf 'works(stdin, true) :- eq(ok, ok).\n' | bin/see -
bin/see https://raw.githubusercontent.com/eyereasoner/see/refs/heads/main/examples/ancestor.pl

The CLI runs directly on Node.js 18 or newer. The browser playground uses the same source modules through playground-worker.mjs; no separate browser build is required.

Serve the playground locally:

python3 -m http.server 8000
# then open http://localhost:8000/playground.html

Running SEE

Show the package version:

bin/see --version
bin/see -v

Run a program and let SEE print derived binary facts with explanations:

bin/see examples/ancestor.pl

Run an explicit query:

bin/see --query 'ancestor(pat, X)' examples/ancestor.pl

SEE-readable explanations are part of the default output. Each why/2 fact contains a nested abstract proof term, and a blank line separates consecutive explanations. Using SEE syntax for explanations keeps them in the same language as the answers themselves: they are readable by humans, parseable by SEE, easy to test, and can be queried, transformed, or explained further like any other SEE data. For example:

type(socrates, mortal).
why(
  type(socrates, mortal),
  proof(
    goal(type(socrates, mortal)),
    by(rule("socrates.pl", clause(4))),
    bindings([binding("X", socrates)]),
    uses([
      proof(
        goal(type(socrates, man)),
        by(fact("socrates.pl", clause(3)))
      )
    ])
  )
).

The explanation output can itself be read as SEE input and queried, for example why(type(socrates, mortal), Proof).

Explanation cookbook

SEE answers carry their own provenance by default.

Explain one derived fact:

bin/see --query 'type(socrates, mortal)' examples/socrates.pl

The output contains the answer and a why/2 fact. The proof term shows the source rule that produced the answer and the source fact used below it. Source references use rule("file.pl", clause(N)) and fact("file.pl", clause(N)), where N is the 1-based clause number in that file.

Inspect variable bindings with a small policy program:

score(case1, 95).
threshold(90).

status(Case, accepted) :-
  score(Case, Score),
  threshold(T),
  ge(Score, T).

bin/see --query 'status(Case, accepted)' policy.pl

The explanation contains the instantiated answer and the variables that made the rule succeed:

status(case1, accepted).
why(
  status(case1, accepted),
  proof(
    goal(status(case1, accepted)),
    by(rule("policy.pl", clause(3))),
    bindings([binding("Case", case1), binding("Score", 95), binding("T", 90)]),
    uses([...])
  )
).

Use the uses([...]) list to follow the proof tree. In the policy example it contains one subproof for score(case1, 95), one for threshold(90), and one for the built-in comparison ge(95, 90). Built-ins are shown as builtin(Name, Arity) because they do not come from source clauses.

Reuse explanations as data:

bin/see --query 'type(socrates, mortal)' examples/socrates.pl > socrates.why.pl
bin/see --query 'why(type(socrates, mortal), Proof)' socrates.why.pl

When a query has no answers, SEE prints no answers and no explanations. That makes missing proofs explicit without inventing a reason.

Compose multiple files, stdin, and URLs:

bin/see facts.pl rules.pl
printf 'works(stdin, true) :- eq(ok, ok).\n' | bin/see -
bin/see https://example.test/program.pl

--query GOAL parses a single goal. Parenthesized conjunctions are accepted:

bin/see --query '(ancestor(pat, X), ancestor(X, emma))' examples/ancestor.pl

Default output

SEE programs write relation predicates directly:

parent(pat, jan).
parent(jan, emma).

ancestor(X, Y) :- parent(X, Y).
ancestor(X, Z) :- parent(X, Y), ancestor(Y, Z).

Without --query, SEE asks for new ground binary consequences of the shape p(S, O), suppresses duplicates, excludes source facts, sorts the result, and prints Prolog facts:

ancestor(jan, emma).
ancestor(pat, emma).
ancestor(pat, jan).

This default is intentionally output-oriented. It is not a complete bottom-up saturation engine. Built-ins and proof search remain goal-directed; use --query when you want a specific relation, arity, or non-binary answer.

Focusing default output

Large examples often have internal helper predicates. Add materialize(Name, Arity). declarations to restrict no-query output to selected predicates:

materialize(answer, 2).

seed(case1).
helper(Case, score(95)) :- seed(Case).
answer(Case, accepted) :- helper(Case, score(95)).

The default output is then:

answer(case1, accepted).

materialize/2 is a declaration, not a logical rule to prove. It does not affect explicit --query answers.

Writing programs

A good SEE program normally has three layers:

1. source facts;
2. helper predicates for calculation or search;
3. concise relation-style outputs, usually binary predicates such as status(Case, Value), reason(Case, Text), ancestor(Person, Ancestor), or cost(Path, Amount).

Example:

score(case1, 95).
threshold(90).

accepted(Case) :-
  score(Case, Score),
  threshold(Threshold),
  ge(Score, Threshold).

status(Case, accepted) :- accepted(Case).
reason(Case, "score exceeds threshold") :- accepted(Case).

When status/2 and reason/2 are derived, they appear in default output. If the program has many helper binary predicates, declare the intended output predicates:

materialize(status, 2).
materialize(reason, 2).

Naming

Predicate names and atom constants use the same lexical form. Namespace-like names should be plain names such as type, person_name, or odrl_permission; colon names are not part of the language.

Queries remain general

The default output focuses on materialized binary facts, but the query engine supports arbitrary goals and arities:

bin/see --query 'append(A, B, [a, b])' examples/list-collection.pl
bin/see --query 'ackermann(4, 2, A)' examples/ackermann.pl
bin/see --query 'once(solution(classic, S))' examples/sudoku.pl

Add --stats when you want lightweight solver counters on stderr without changing stdout:

bin/see --stats --query 'once(solution(classic, S))' examples/sudoku.pl

The playground has a matching --stats checkbox, so browser runs can show the same counters in the combined output window.

Builtins

SEE builtins are registered by name and arity in small modules under src/builtins. This keeps the runtime portable to Node.js and the browser while giving each builtin family a clear boundary. Builtins are enabled by normal predicate calls.

The core builtin families cover unification, arithmetic, comparison, dates, strings, lists, aggregation, formula terms, and search control. Additional reusable finite-search helpers are available for examples that would otherwise need large amounts of repetitive generate-and-test code. These helpers are deliberately general relations rather than shortcuts tied to a particular example name. For example:

solution(Name, Rows) :-
  puzzle(Name, Grid),
  sudoku(Grid, Rows).

answer(Queens) :-
  n_queens(8, Queens).

best(Cycle, Cost) :-
  cities(Cities),
  weighted_hamiltonian_cycle(edge, Cities, Cycle, Cost).

sudoku/2 accepts either an 81-character string or a 9x9 list. Digits 1 to 9 are givens; 0, ., and _ mark blanks. It returns the solved 9x9 list.

The reusable search and numeric helpers include atom_range/4, atom_ranges/4, n_queens/2, Hamiltonian path/cycle helpers, cnf_model/3, Quine-McCluskey helpers, bounded subset/path helpers, number-theory helpers such as extended_gcd/5, matrix helpers such as matrix_multiply/2, and alphametic_sum/5. These helpers are extension builtins of this implementation; SPEC.md defines the portable core and standard builtin profile.

To add a builtin, create or extend a module with register(registry) and call registry.add(name, arity, handler, options). The default registry is assembled in src/builtins/registry.js. Builtins that are only safe for specific argument modes should provide a ready predicate and fallbackWhenNotReady: true, so user-defined clauses remain visible until the builtin is applicable.

Aggregation helpers

SEE includes goal-directed aggregation helpers for finite searches:

countall(Goal, Count).
sumall(Value, Goal, Sum).
aggregate_min(Key, Template, Goal, BestKey, BestTemplate).
aggregate_max(Key, Template, Goal, BestKey, BestTemplate).

Use countall/2 for solution counts, sumall/3 for numeric totals, and aggregate_min/5 or aggregate_max/5 when a search should keep only the best candidate instead of collecting and sorting every answer. The Key can be a number, atom constant, string, compound term, or list; normal term ordering is used, so compound keys such as [Cost, Path] are useful for deterministic tie-breaking.

Example:

best_cycle(Cycle, Cost) :-
  cities(Cities),
  aggregate_min([Cost, Cycle], Cycle, candidate_cycle(Cities, Cycle, Cost), [Cost, Cycle], Cycle).

Formula data

Comma terms can be data as well as conjunctions. SEE provides relation-oriented formula utilities.

formula_atom(Formula, Atom) enumerates atomic formula terms inside a comma formula:

formula_atom((name(alice, "Alice"), knows(alice, bob)), X).

formula_binary(Formula, S, P, O) enumerates binary terms and exposes their functor as an atom constant:

formula_binary((name(alice, "Alice"), knows(alice, bob)), S, P, O).

This can yield S = alice, P = name, O = "Alice" and S = alice, P = knows, O = bob. The utility is useful for quoted formula data, but it does not make those formula members true in the ambient program.

Example catalog

The repository includes examples for recursion, graph reachability, finite search, arithmetic, list processing, optimization, policies, puzzles, N3-inspired rule chains, and applied scientific calculations. Bundled examples use relation-style output.

| Input | Short description | Output | | --- | --- | --- | | access-control-policy.pl | Evaluates role and condition based access decisions. | output/access-control-policy.pl | | ackermann.pl | Computes Ackermann-style hyperoperation values. | output/ackermann.pl | | age.pl | Checks whether people meet age thresholds. | output/age.pl | | aliases-and-namespaces.pl | Shows ordinary predicate names for vocabulary aliases. | output/aliases-and-namespaces.pl | | alignment-demo.pl | Rolls dataset concepts up through a small alignment taxonomy. | output/alignment-demo.pl | | allen-interval-calculus.pl | Classifies interval relations with integer time offsets. | output/allen-interval-calculus.pl | | ancestor.pl | Derives ancestors from parent facts. | output/ancestor.pl | | animal.pl | Classifies animals from traits. | output/animal.pl | | annotation.pl | Derives facts from quoted annotation data. | output/annotation.pl | | backward.pl | Shows a backward-rule pattern as a goal-directed numeric rule. | output/backward.pl | | basic-monadic.pl | Runs a monadic benchmark over generated inputs. | output/basic-monadic.pl | | bayes-diagnosis.pl | Computes scaled Bayesian diagnosis posteriors. | output/bayes-diagnosis.pl | | bayes-therapy.pl | Ranks therapies using Bayesian disease likelihoods. | output/bayes-therapy.pl | | beam-deflection.pl | Computes cantilever beam deflection. | output/beam-deflection.pl | | blocks-world-planning.pl | Searches a finite blocks-world plan. | output/blocks-world-planning.pl | | bmi.pl | Normalizes BMI inputs and classifies weight. | output/bmi.pl | | braking-safety-worlds.pl | Classifies braking safety under alternative worlds. | output/braking-safety-worlds.pl | | buck-converter-design.pl | Checks buck-converter ripple design. | output/buck-converter-design.pl | | cache-performance.pl | Summarizes cache latency performance. | output/cache-performance.pl | | canary-release.pl | Decides canary rollout or rollback. | output/canary-release.pl | | cat-koko.pl | Demonstrates named existential witnesses from a Cat Koko rule pattern. | output/cat-koko.pl | | clinical-trial-screening.pl | Screens candidates for a trial. | output/clinical-trial-screening.pl | | collatz-1000.pl | Computes shared Collatz trajectories. | output/collatz-1000.pl | | combinatorics-findall-sort.pl | Collects and sorts finite combinations. | output/combinatorics-findall-sort.pl | | competitive-enzyme-kinetics.pl | Computes inhibited enzyme reaction rates. | output/competitive-enzyme-kinetics.pl | | complex-matrix-stability.pl | Checks stability of a 2x2 system. | output/complex-matrix-stability.pl | | complex.pl | Performs arithmetic on complex pairs. | output/complex.pl | | composition-of-injective-functions-is-injective.pl | Encodes composition and injectivity of finite functions. | output/composition-of-injective-functions-is-injective.pl | | context-association.pl | Associates named contexts with their contents. | output/context-association.pl | | control-system.pl | Evaluates control-system measurements and targets. | output/control-system.pl | | cryptarithmetic-send-more-money.pl | Solves SEND+MORE and related puzzles. | output/cryptarithmetic-send-more-money.pl | | cyclic-path.pl | Computes paths in a cyclic graph. | output/cyclic-path.pl | | d3-group.pl | Enumerates subgroups of the D3 group. | output/d3-group.pl | | dairy-energy-balance.pl | Classifies dairy cow energy balance. | output/dairy-energy-balance.pl | | data-negotiation.pl | Chooses an accepted data-negotiation offer. | output/data-negotiation.pl | | deep-taxonomy-10.pl | Stress-tests recursive taxonomy depth 10. | output/deep-taxonomy-10.pl | | deep-taxonomy-100.pl | Stress-tests recursive taxonomy depth 100. | output/deep-taxonomy-100.pl | | deep-taxonomy-1000.pl | Stress-tests recursive taxonomy depth 1000. | output/deep-taxonomy-1000.pl | | deep-taxonomy-10000.pl | Stress-tests recursive taxonomy depth 10000. | output/deep-taxonomy-10000.pl | | deep-taxonomy-100000.pl | Stress-tests recursive taxonomy depth 100000. | output/deep-taxonomy-100000.pl | | delfour.pl | Derives shopping and authorization recommendations. | output/delfour.pl | | dense-hamiltonian-cycle.pl | Searches a dense Hamiltonian cycle with aggregate minimization. | output/dense-hamiltonian-cycle.pl | | deontic-logic.pl | Reports obligations, prohibitions, and violations. | output/deontic-logic.pl | | derived-rule.pl | Derives conclusions from rule data. | output/derived-rule.pl | | diamond-property.pl | Checks the diamond property of a relation. | output/diamond-property.pl | | dijkstra-findall-sort.pl | Finds shortest paths using collected candidates. | output/dijkstra-findall-sort.pl | | dijkstra-risk-path.pl | Ranks routes by cost and trust. | output/dijkstra-risk-path.pl | | dijkstra.pl | Enumerates weighted simple paths. | output/dijkstra.pl | | dining-philosophers.pl | Simulates Chandy-Misra fork exchanges. | output/dining-philosophers.pl | | dog.pl | Counts dogs and derives when a license is required. | output/dog.pl | | drone-corridor-planner.pl | Plans bounded drone corridor routes. | output/drone-corridor-planner.pl | | easter-computus.pl | Computes Gregorian Easter dates. | output/easter-computus.pl | | electrical-rc-filter.pl | Sizes an RC low-pass filter. | output/electrical-rc-filter.pl | | epidemic-policy.pl | Chooses policies from risk and social cost. | output/epidemic-policy.pl | | equivalence-classes-overlap-implies-same-class.pl | Packages the shared-member proof pattern for equivalence classes. | output/equivalence-classes-overlap-implies-same-class.pl | | eulerian-path.pl | Finds an Eulerian path using each edge once. | output/eulerian-path.pl | | ev-range-worlds.pl | Estimates electric-vehicle trip feasibility. | output/ev-range-worlds.pl | | exact-cover-sudoku.pl | Solves Sudoku via exact-cover-style constraints. | output/exact-cover-sudoku.pl | | existential-rule.pl | Represents existential witnesses with explicit Skolem-style terms. | output/existential-rule.pl | | exoplanet-validation-worlds.pl | Validates exoplanet candidates across worlds. | output/exoplanet-validation-worlds.pl | | expression-eval.pl | Evaluates a small arithmetic expression tree. | output/expression-eval.pl | | family-cousins.pl | Derives cousin and family labels. | output/family-cousins.pl | | fastpow.pl | Computes powers by repeated squaring. | output/fastpow.pl | | fft8-numeric.pl | Runs an 8-point FFT over complex pairs. | output/fft8-numeric.pl | | fibonacci.pl | Computes large Fibonacci numbers by fast doubling. | output/fibonacci.pl | | field-nitrogen-balance.pl | Classifies field nitrogen balance. | output/field-nitrogen-balance.pl | | floating-point.pl | Exercises floating-point arithmetic and comparisons. | output/floating-point.pl | | four-color-map.pl | Checks a four-colour map assignment. | output/four-color-map.pl | | fundamental-theorem-arithmetic.pl | Factors integers and reconstructs products. | output/fundamental-theorem-arithmetic.pl | | gcd-bezout-identity.pl | Computes gcd and Bézout coefficients. | output/gcd-bezout-identity.pl | | gd-step-certified.pl | Certifies a gradient-descent step. | output/gd-step-certified.pl | | gdpr-compliance.pl | Checks GDPR-style processing compliance. | output/gdpr-compliance.pl | | goldbach-1000.pl | Finds Goldbach prime pairs up to 1000. | output/goldbach-1000.pl | | good-cobbler.pl | Demonstrates term-level structure with a good-cobbler statement. | output/good-cobbler.pl | | gps.pl | Finds and verifies route paths. | output/gps.pl | | graph-reachability.pl | Derives reachable nodes in a graph. | output/graph-reachability.pl | | gray-code-counter.pl | Generates Gray-code counter states. | output/gray-code-counter.pl | | greatest-lower-bound-uniqueness.pl | Shows uniqueness of greatest lower bounds in a finite order instance. | output/greatest-lower-bound-uniqueness.pl | | group-inverse-uniqueness.pl | Shows uniqueness of inverses in a finite group instance. | output/group-inverse-uniqueness.pl | | hamiltonian-cycle.pl | Finds a Hamiltonian cycle. | output/hamiltonian-cycle.pl | | hamiltonian-path.pl | Finds a Hamiltonian path. | output/hamiltonian-path.pl | | hamming-code.pl | Corrects a single-bit Hamming word. | output/hamming-code.pl | | hanoi.pl | Derives the Towers of Hanoi moves. | output/hanoi.pl | | heat-loss.pl | Computes conductive heat loss. | output/heat-loss.pl | | heron-theorem.pl | Computes triangle area by Heron's theorem. | output/heron-theorem.pl | | ideal-gas-law.pl | Applies the ideal gas law. | output/ideal-gas-law.pl | | illegitimate-reasoning.pl | Detects suspect reasoning patterns. | output/illegitimate-reasoning.pl | | kaprekar.pl | Iterates toward Kaprekar's constant. | output/kaprekar.pl | | law-of-cosines.pl | Computes a triangle side by cosine law. | output/law-of-cosines.pl | | least-squares-regression.pl | Fits a least-squares regression line. | output/least-squares-regression.pl | | list-collection.pl | Demonstrates list and collection built-ins. | output/list-collection.pl | | lldm.pl | Calculates leg-length discrepancy measurements. | output/lldm.pl | | manufacturing-quality-control.pl | Evaluates process capability and quality. | output/manufacturing-quality-control.pl | | matrix.pl | Runs matrix operations over sample inputs. | output/matrix.pl | | microgrid-dispatch.pl | Plans microgrid dispatch and reserve. | output/microgrid-dispatch.pl | | monkey-bananas.pl | Solves the monkey-and-bananas puzzle. | output/monkey-bananas.pl | | n-queens.pl | Searches for N-queens placements. | output/n-queens.pl | | network-sla.pl | Checks network path SLA compliance. | output/network-sla.pl | | newton-raphson.pl | Finds roots by Newton-Raphson iteration. | output/newton-raphson.pl | | nixon-diamond.pl | Reports the classic Nixon-diamond conflict. | output/nixon-diamond.pl | | odrl-dpv-healthcare-risk-ranked.pl | Ranks healthcare policy risks and mitigations. | output/odrl-dpv-healthcare-risk-ranked.pl | | odrl-dpv-risk-ranked.pl | Ranks data-policy risks and mitigations. | output/odrl-dpv-risk-ranked.pl | | orbital-transfer-design.pl | Designs a Hohmann orbital transfer. | output/orbital-transfer-design.pl | | path-discovery.pl | Discovers bounded air-route paths. | output/path-discovery.pl | | peano-arithmetic.pl | Computes Peano addition, multiplication, and factorial. | output/peano-arithmetic.pl | | peasant.pl | Performs peasant multiplication and exponentiation. | output/peasant.pl | | pendulum-period.pl | Computes simple pendulum periods. | output/pendulum-period.pl | | polynomial.pl | Finds complex integer polynomial roots. | output/polynomial.pl | | project-portfolio-optimization.pl | Optimizes a constrained project portfolio with pruning and aggregate builtins. | output/project-portfolio-optimization.pl | | proof-contrapositive.pl | Models proof by contrapositive. | output/proof-contrapositive.pl | | quadratic-formula.pl | Solves sample quadratic equations. | output/quadratic-formula.pl | | quine-mccluskey.pl | Minimizes Boolean terms with Quine-McCluskey. | output/quine-mccluskey.pl | | radioactive-decay.pl | Computes radioactive decay over time. | output/radioactive-decay.pl | | sat-dpll.pl | Solves a finite SAT instance. | output/sat-dpll.pl | | security-incident-correlation.pl | Correlates security incidents across signals. | output/security-incident-correlation.pl | | service-impact.pl | Analyzes service impact over cyclic dependencies. | output/service-impact.pl | | sieve.pl | Enumerates primes with a sieve-style program. | output/sieve.pl | | skolem-functions.pl | Generates deterministic functional terms. | output/skolem-functions.pl | | socrates.pl | Derives that Socrates is mortal. | output/socrates.pl | | statistics-summary.pl | Computes population statistics for a sample. | output/statistics-summary.pl | | sudoku.pl | Solves generic 9x9 Sudoku strings through the sudoku/2 builtin. | output/sudoku.pl | | superdense-coding.pl | Models superdense-coding bit transmission. | output/superdense-coding.pl | | traveling-salesman.pl | Finds an optimal traveling-salesman tour. | output/traveling-salesman.pl | | turing.pl | Simulates a binary-increment Turing machine. | output/turing.pl | | vector-similarity.pl | Computes dot product, norm, and cosine similarity. | output/vector-similarity.pl | | witch.pl | Derives the classic “burn the witch” N3 rule chain. | output/witch.pl | | wolf-goat-cabbage.pl | Solves the wolf-goat-cabbage river crossing. | output/wolf-goat-cabbage.pl | | zebra.pl | Solves the zebra logic puzzle. | output/zebra.pl |

Golden outputs, tests, and conformance

Golden outputs live in examples/output. They include both answer facts and their why/2 explanations. Example tests pin local_time/1 to 2026-05-30 so date-dependent examples stay deterministic. Regenerate them after an intentional output or explanation change:

for f in examples/*.pl; do
  b=$(basename "$f")
  SEE_LOCAL_TIME=2026-05-30 bin/see "$f" > "examples/output/$b"
done

Run the full test suite:

npm test

The test suite runs in this order: Conformance, Regression/API/White-box, Examples. Each section prints its own subtotal, followed by a suite-specific grand total. The suite checks the conformance cases derived from SPEC.md, supplemental regression/API/white-box checks, and every example against its explanation-rich output golden.

Run only one suite when you are iterating:

npm run test:conformance
npm run test:regression
npm run test:examples

The conformance suite lives in conformance/ and is split into core and extension profiles matching SPEC.md. Each case is a small program with optional query text and an exact expected stdout file, so other implementations can reuse the same cases. The regression suite lives in test/run-regression.js and covers CLI regressions, the public JavaScript API, and white-box invariants for parser, unification, and indexing behavior.

Development and release

Common commands:

npm test                  # conformance, regression/API/white-box, and examples
npm run test:conformance  # only the conformance suite
npm run test:regression   # CLI regression, API, and white-box checks
npm run test:examples     # every example against examples/output
node bin/see --help

Useful profiling smoke test:

bin/see --stats --query 'once(solution(classic, S))' examples/sudoku.pl > /dev/null

For a release:

1. update VERSION;
2. update README.md and SPEC.md;
3. regenerate golden outputs if behavior changed;
4. run npm test;
5. publish the repository with playground.html and playground-worker.mjs if publishing the playground. The playground includes controls equivalent to CLI --query GOAL and --stats.

Performance notes

Use --stats for a quick sanity check while optimizing solver changes. It prints counters such as solve_goals_calls, unify_calls, deterministic_rule_expansions, candidate_lists_selected, clause_candidates_considered, clauses_tried, max_depth, and max_solver_call_depth to stderr, leaving normal output stable for golden-file tests. The max_solver_call_depth counter is especially useful for browser regressions, where the VM call stack can be tighter than a command-line run.

SEE hashes predicate groups by name and arity, then indexes clauses by scalar argument values. It also builds two-argument composite indexes for scalar pairs and probes those composite indexes without per-lookup heap allocation. This helps both large generated programs with many predicates and selective queries such as:

edge(g1, a, X).
path(a, Y).
status(Case, accepted).

Ground facts use a fast path that avoids freshening and copying a rule body. Recursive-predicate detection uses an explicit work stack, which keeps large predicate chains safer in the browser. Recursive examples use an active-call variant guard to prevent common cyclic closures from looping. Selected predicates can be memoized with:

memoize(path, 2).

For large programs, keep helper predicates selective, bind arguments early, and declare focused output predicates with materialize/2 when default output would otherwise ask broad helper queries.

Implementation limits

SEE is intentionally smaller than ISO Prolog. It has no operators, cut, modules, dynamic database updates, DCGs, or complete ISO library. Negation is negation-as-failure through not/1. Search is goal-directed and expected to be finite for the supplied program and query. Output explanations are non-normative proof printouts and do not change answer semantics.