# SEE Guide

This guide introduces SEE, the **Symbolic English Engine**: a compact reasoning engine for facts, rules, goals, answers, and proofs. SEE works over ordinary terms, lists, arithmetic, strings, and finite search. Run it with the `see` CLI, or use `node bin/see.js` from a source checkout.

Programs write relations as Symbolic English statements, for example `ancestor holds for pat and emma` or `status holds for case1 and accepted`. Use `show facts for status with 2 values` to focus output on a relation. By default, the CLI prints derived ground facts in the same Symbolic English syntax it accepts as input. Pass `--proof` or `-p` to emit compact readable `explanation holds for "..."` proof summaries.

For the normative language definition, including lexical syntax, terms, clauses, goals, built-ins, `show`, tabling declarations, and conformance boundaries, read the [SEE language reference](language-reference.md).

## Contents

1. [Quick start](#quick-start)
2. [Running see](#running-see)
3. [Default output](#default-output)
4. [Writing programs](#writing-programs)
5. [Aggregation helpers](#aggregation-helpers)
6. [Context data](#context-data)
7. [Example catalog](#example-catalog)
8. [Golden outputs, tests, and conformance](#golden-outputs-tests-and-conformance)
9. [Development and release](#development-and-release)
10. [Relationship to Eyeling](#relationship-to-eyeling)
11. [Performance notes](#performance-notes)
12. [Implementation limits](#implementation-limits)

## Quick start

SEE has no runtime npm dependencies and no build step. From a source checkout, run the CLI entry point directly with Node.js 18 or newer:

```sh
node bin/see.js --version
node bin/see.js examples/ancestor.see
node bin/see.js facts.see rules.see
printf 'works holds for stdin and true if eq holds for ok and ok
' | node bin/see.js -
```

You can also use npm's local package-bin runner from the checkout:

```sh
npm exec -- see --version
npm exec -- see examples/ancestor.see
```

To make the `see` command available on your `PATH` while developing this checkout, prefer npm's package link instead of a manual symlink:

```sh
npm link
see --version
```

## Running see

The commands in this section use `see` for readability. In a source checkout where you have not run `npm link`, replace `see` with `node bin/see.js`, or run the command through `npm exec -- see`.

Show the package version:

```sh
see --version
see -v
```

Run a program and let SEE print derived facts:

```sh
see examples/ancestor.see
```

Enable proof explanations if you want readable provenance:

```sh
see --proof examples/ancestor.see
see -p examples/ancestor.see
```

A proof run keeps the answer facts in ordinary Symbolic English and follows each answer with a short `explanation` summary:

```see
type holds for socrates and mortal
explanation holds for "because rule socrates.see:4; uses type/2 via fact socrates.see:2"
```

The compact proof output can itself be read as SEE input because each explanation is an `explanation holds for "..."` fact. Use `--proof=tree` for an indented human proof tree with shortened terms, or `--proof=full` for the complete nested SEE proof data used by tooling that needs every proof node and binding. Proof output is additional data; it does not change the answers found by the solver.

## Default output

A small family program looks like this:

```see
show facts for ancestor with 2 values
parent holds for pat and jan
parent holds for jan and emma
ancestor holds for ?x and ?y if parent holds for ?x and ?y
ancestor holds for ?x and ?z if parent holds for ?x and ?y and ancestor holds for ?y and ?z
```

The default output is Symbolic English too:

```see
ancestor holds for jan and emma
ancestor holds for pat and emma
ancestor holds for pat and 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 `show facts for name with arity values` declarations and small output relations if you want a specific relation or arity.

### Focusing default output

Large examples often have internal helper relations. Add `show` declarations to restrict default output:

```see
show facts for answer with 2 values
seed holds for case1
helper holds for ?case and the fact that score holds for 95 end if seed holds for ?case
answer holds for ?case and accepted if helper holds for ?case and the fact that score holds for 95 end
```

The default output is then:

```see
answer holds for case1 and accepted
```

`show` is a declaration, not a logical rule to prove. It affects which relations the CLI prints, not the meaning of the rules themselves.

## Writing programs

A good SEE program normally holds for three layers: source facts, helper relations for calculation or search, and concise output relations such as `status holds for ?case and accepted`, `reason holds for ?case and "score exceeds threshold"`, or `cost holds for ?path and ?amount`.

Example:

```see
show facts for status with 2 values
show facts for reason with 2 values
score holds for case1 and 95
threshold holds for 90
accepted holds for ?case if score holds for ?case and ?score and threshold holds for ?threshold and ge holds for ?score and ?threshold
status holds for ?case and accepted if accepted holds for ?case
reason holds for ?case and "score exceeds threshold" if accepted holds for ?case
```

### 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`, or backtick-quoted atoms if punctuation is needed.

### Builtins

SEE builtins are registered by name and arity in small modules under [`src/builtins`](../src/builtins). This keeps the runtime portable to Node.js and the browser while giving each builtin family a clear boundary. Built-ins are called as Symbolic English relations. The bundled implementation currently registers 80 name/arity entries across 78 predicate names:

| Builtin | Notes |
| --- | --- |
| `abs/2` | Built-in relation available to SEE programs. |
| `acos/2` | Built-in relation available to SEE programs. |
| `add/3` | Built-in relation available to SEE programs. |
| `aggregate_max/5` | Built-in relation available to SEE programs. |
| `aggregate_min/5` | Built-in relation available to SEE programs. |
| `append/3` | Built-in relation available to SEE programs. |
| `arg/3` | Built-in relation available to SEE programs. |
| `asin/2` | Built-in relation available to SEE programs. |
| `atan2/3` | Built-in relation available to SEE programs. |
| `atom_string/2` | Built-in relation available to SEE programs. |
| `between/3` | Built-in relation available to SEE programs. |
| `ceiling/2` | Built-in relation available to SEE programs. |
| `compound_name_arguments/3` | Built-in relation available to SEE programs. |
| `contains/2` | Built-in relation available to SEE programs. |
| `cos/2` | Built-in relation available to SEE programs. |
| `countall/2` | Built-in relation available to SEE programs. |
| `difference/3` | Built-in relation available to SEE programs. |
| `div/3` | Built-in relation available to SEE programs. |
| `drop/3` | Built-in relation available to SEE programs. |
| `eq/2` | Built-in relation available to SEE programs. |
| `exp/2` | Built-in relation available to SEE programs. |
| `findall/3` | Built-in relation available to SEE programs. |
| `floor/2` | Built-in relation available to SEE programs. |
| `forall/2` | Built-in relation available to SEE programs. |
| `functor/3` | Built-in relation available to SEE programs. |
| `ge/2` | Built-in relation available to SEE programs. |
| `gt/2` | Built-in relation available to SEE programs. |
| `head/2` | Built-in relation available to SEE programs. |
| `holds/2` | Built-in relation available to SEE programs. |
| `holds/3` | Built-in relation available to SEE programs. |
| `join/3` | Built-in relation available to SEE programs. |
| `last/2` | Built-in relation available to SEE programs. |
| `le/2` | Built-in relation available to SEE programs. |
| `length/2` | Built-in relation available to SEE programs. |
| `list_to_set/2` | Built-in relation available to SEE programs. |
| `local_time/1` | Built-in relation available to SEE programs. |
| `log/2` | Built-in relation available to SEE programs. |
| `lowercase/2` | Built-in relation available to SEE programs. |
| `lt/2` | Built-in relation available to SEE programs. |
| `matches/2` | Built-in relation available to SEE programs. |
| `matches/3` | Built-in relation available to SEE programs. |
| `max/3` | Built-in relation available to SEE programs. |
| `max_list/2` | Built-in relation available to SEE programs. |
| `member/2` | Built-in relation available to SEE programs. |
| `min/3` | Built-in relation available to SEE programs. |
| `min_list/2` | Built-in relation available to SEE programs. |
| `mod/3` | Built-in relation available to SEE programs. |
| `mul/3` | Built-in relation available to SEE programs. |
| `neg/2` | Built-in relation available to SEE programs. |
| `neq/2` | Built-in relation available to SEE programs. |
| `not/1` | Built-in relation available to SEE programs. |
| `not_matches/2` | Built-in relation available to SEE programs. |
| `not_member/2` | Built-in relation available to SEE programs. |
| `nth0/3` | Built-in relation available to SEE programs. |
| `number_string/2` | Built-in relation available to SEE programs. |
| `once/1` | Built-in relation available to SEE programs. |
| `pow/3` | Built-in relation available to SEE programs. |
| `replace/4` | Built-in relation available to SEE programs. |
| `rest/2` | Built-in relation available to SEE programs. |
| `reverse/2` | Built-in relation available to SEE programs. |
| `rounded/2` | Built-in relation available to SEE programs. |
| `select/3` | Built-in relation available to SEE programs. |
| `set_nth0/4` | Built-in relation available to SEE programs. |
| `sin/2` | Built-in relation available to SEE programs. |
| `slice/4` | Built-in relation available to SEE programs. |
| `smallest_divisor_from/3` | Built-in relation available to SEE programs. |
| `sort/2` | Built-in relation available to SEE programs. |
| `split/3` | Built-in relation available to SEE programs. |
| `sqrt/2` | Built-in relation available to SEE programs. |
| `str_concat/3` | Built-in relation available to SEE programs. |
| `sub/3` | Built-in relation available to SEE programs. |
| `substring/4` | Built-in relation available to SEE programs. |
| `sum_list/2` | Built-in relation available to SEE programs. |
| `sumall/3` | Built-in relation available to SEE programs. |
| `take/3` | Built-in relation available to SEE programs. |
| `tan/2` | Built-in relation available to SEE programs. |
| `term_string/2` | Built-in relation available to SEE programs. |
| `trim/2` | Built-in relation available to SEE programs. |
| `trunc/2` | Built-in relation available to SEE programs. |
| `uppercase/2` | Built-in relation available to SEE programs. |

## Aggregation helpers

Aggregation helpers are ordinary built-ins. Use `countall/2` for solution counts, `sumall/3` for numeric totals, and `aggregate_min/5` or `aggregate_max/5` if a search should keep only the best candidate instead of collecting and sorting every answer.

```see
show facts for best_cycle with 2 values
best_cycle holds for ?cycle and ?cost if cities holds for ?cities and aggregate_min holds for the list of ?cost and ?cycle end and ?cycle and the candidate_cycle holds for ?cities and ?cycle and ?cost end and the list of ?cost and ?cycle end and ?cycle
```

## Context data

Context helpers let a program inspect compound data without making that data true globally. For example, `holds/2` can match a member term directly, and `holds/3` exposes a member's name and argument list as data. See [`context-schema-audit.see`](../examples/context-schema-audit.see) for a schema-audit example.

## Example catalog

| Source | Description | Golden output |
| --- | --- | --- |
| [`abstract-interpretation.see`](../examples/abstract-interpretation.see) | Runnable Symbolic English example. | [`output/abstract-interpretation.see`](../examples/output/abstract-interpretation.see) |
| [`access-control-policy.see`](../examples/access-control-policy.see) | Runnable Symbolic English example. | [`output/access-control-policy.see`](../examples/output/access-control-policy.see) |
| [`ackermann.see`](../examples/ackermann.see) | Runnable Symbolic English example. | [`output/ackermann.see`](../examples/output/ackermann.see) |
| [`age.see`](../examples/age.see) | Runnable Symbolic English example. | [`output/age.see`](../examples/output/age.see) |
| [`aliases-and-namespaces.see`](../examples/aliases-and-namespaces.see) | Runnable Symbolic English example. | [`output/aliases-and-namespaces.see`](../examples/output/aliases-and-namespaces.see) |
| [`alignment-demo.see`](../examples/alignment-demo.see) | Runnable Symbolic English example. | [`output/alignment-demo.see`](../examples/output/alignment-demo.see) |
| [`allen-interval-calculus.see`](../examples/allen-interval-calculus.see) | Runnable Symbolic English example. | [`output/allen-interval-calculus.see`](../examples/output/allen-interval-calculus.see) |
| [`ancestor.see`](../examples/ancestor.see) | Runnable Symbolic English example. | [`output/ancestor.see`](../examples/output/ancestor.see) |
| [`animal.see`](../examples/animal.see) | Runnable Symbolic English example. | [`output/animal.see`](../examples/output/animal.see) |
| [`annotation.see`](../examples/annotation.see) | Runnable Symbolic English example. | [`output/annotation.see`](../examples/output/annotation.see) |
| [`auroracare.see`](../examples/auroracare.see) | Runnable Symbolic English example. | [`output/auroracare.see`](../examples/output/auroracare.see) |
| [`backward.see`](../examples/backward.see) | Runnable Symbolic English example. | [`output/backward.see`](../examples/output/backward.see) |
| [`basic-monadic.see`](../examples/basic-monadic.see) | Runnable Symbolic English example. | [`output/basic-monadic.see`](../examples/output/basic-monadic.see) |
| [`bayes-diagnosis.see`](../examples/bayes-diagnosis.see) | Runnable Symbolic English example. | [`output/bayes-diagnosis.see`](../examples/output/bayes-diagnosis.see) |
| [`bayes-therapy.see`](../examples/bayes-therapy.see) | Runnable Symbolic English example. | [`output/bayes-therapy.see`](../examples/output/bayes-therapy.see) |
| [`beam-deflection.see`](../examples/beam-deflection.see) | Runnable Symbolic English example. | [`output/beam-deflection.see`](../examples/output/beam-deflection.see) |
| [`binomial-vandermonde.see`](../examples/binomial-vandermonde.see) | Runnable Symbolic English example. | [`output/binomial-vandermonde.see`](../examples/output/binomial-vandermonde.see) |
| [`blocks-world-planning.see`](../examples/blocks-world-planning.see) | Runnable Symbolic English example. | [`output/blocks-world-planning.see`](../examples/output/blocks-world-planning.see) |
| [`bmi.see`](../examples/bmi.see) | Runnable Symbolic English example. | [`output/bmi.see`](../examples/output/bmi.see) |
| [`braking-safety-worlds.see`](../examples/braking-safety-worlds.see) | Runnable Symbolic English example. | [`output/braking-safety-worlds.see`](../examples/output/braking-safety-worlds.see) |
| [`buck-converter-design.see`](../examples/buck-converter-design.see) | Runnable Symbolic English example. | [`output/buck-converter-design.see`](../examples/output/buck-converter-design.see) |
| [`cache-performance.see`](../examples/cache-performance.see) | Runnable Symbolic English example. | [`output/cache-performance.see`](../examples/output/cache-performance.see) |
| [`canary-release.see`](../examples/canary-release.see) | Runnable Symbolic English example. | [`output/canary-release.see`](../examples/output/canary-release.see) |
| [`cat-koko.see`](../examples/cat-koko.see) | Runnable Symbolic English example. | [`output/cat-koko.see`](../examples/output/cat-koko.see) |
| [`catalan-convolution.see`](../examples/catalan-convolution.see) | Runnable Symbolic English example. | [`output/catalan-convolution.see`](../examples/output/catalan-convolution.see) |
| [`cdcl-sat-solver.see`](../examples/cdcl-sat-solver.see) | Runnable Symbolic English example. | [`output/cdcl-sat-solver.see`](../examples/output/cdcl-sat-solver.see) |
| [`chart-parser.see`](../examples/chart-parser.see) | Runnable Symbolic English example. | [`output/chart-parser.see`](../examples/output/chart-parser.see) |
| [`clinical-trial-screening.see`](../examples/clinical-trial-screening.see) | Runnable Symbolic English example. | [`output/clinical-trial-screening.see`](../examples/output/clinical-trial-screening.see) |
| [`collatz-1000.see`](../examples/collatz-1000.see) | Runnable Symbolic English example. | [`output/collatz-1000.see`](../examples/output/collatz-1000.see) |
| [`combinatorics-findall-sort.see`](../examples/combinatorics-findall-sort.see) | Runnable Symbolic English example. | [`output/combinatorics-findall-sort.see`](../examples/output/combinatorics-findall-sort.see) |
| [`competitive-enzyme-kinetics.see`](../examples/competitive-enzyme-kinetics.see) | Runnable Symbolic English example. | [`output/competitive-enzyme-kinetics.see`](../examples/output/competitive-enzyme-kinetics.see) |
| [`complex.see`](../examples/complex.see) | Runnable Symbolic English example. | [`output/complex.see`](../examples/output/complex.see) |
| [`composition-of-injective-functions-is-injective.see`](../examples/composition-of-injective-functions-is-injective.see) | Runnable Symbolic English example. | [`output/composition-of-injective-functions-is-injective.see`](../examples/output/composition-of-injective-functions-is-injective.see) |
| [`context-association.see`](../examples/context-association.see) | Runnable Symbolic English example. | [`output/context-association.see`](../examples/output/context-association.see) |
| [`context-schema-audit.see`](../examples/context-schema-audit.see) | Runnable Symbolic English example. | [`output/context-schema-audit.see`](../examples/output/context-schema-audit.see) |
| [`continued-fraction-sqrt2.see`](../examples/continued-fraction-sqrt2.see) | Runnable Symbolic English example. | [`output/continued-fraction-sqrt2.see`](../examples/output/continued-fraction-sqrt2.see) |
| [`control-system.see`](../examples/control-system.see) | Runnable Symbolic English example. | [`output/control-system.see`](../examples/output/control-system.see) |
| [`critical-path-schedule.see`](../examples/critical-path-schedule.see) | Runnable Symbolic English example. | [`output/critical-path-schedule.see`](../examples/output/critical-path-schedule.see) |
| [`cyclic-path.see`](../examples/cyclic-path.see) | Runnable Symbolic English example. | [`output/cyclic-path.see`](../examples/output/cyclic-path.see) |
| [`d3-group.see`](../examples/d3-group.see) | Runnable Symbolic English example. | [`output/d3-group.see`](../examples/output/d3-group.see) |
| [`dairy-energy-balance.see`](../examples/dairy-energy-balance.see) | Runnable Symbolic English example. | [`output/dairy-energy-balance.see`](../examples/output/dairy-energy-balance.see) |
| [`data-negotiation.see`](../examples/data-negotiation.see) | Runnable Symbolic English example. | [`output/data-negotiation.see`](../examples/output/data-negotiation.see) |
| [`deep-taxonomy-10.see`](../examples/deep-taxonomy-10.see) | Runnable Symbolic English example. | [`output/deep-taxonomy-10.see`](../examples/output/deep-taxonomy-10.see) |
| [`deep-taxonomy-100.see`](../examples/deep-taxonomy-100.see) | Runnable Symbolic English example. | [`output/deep-taxonomy-100.see`](../examples/output/deep-taxonomy-100.see) |
| [`deep-taxonomy-1000.see`](../examples/deep-taxonomy-1000.see) | Runnable Symbolic English example. | [`output/deep-taxonomy-1000.see`](../examples/output/deep-taxonomy-1000.see) |
| [`deep-taxonomy-10000.see`](../examples/deep-taxonomy-10000.see) | Runnable Symbolic English example. | [`output/deep-taxonomy-10000.see`](../examples/output/deep-taxonomy-10000.see) |
| [`deep-taxonomy-100000.see`](../examples/deep-taxonomy-100000.see) | Runnable Symbolic English example. | [`output/deep-taxonomy-100000.see`](../examples/output/deep-taxonomy-100000.see) |
| [`delfour.see`](../examples/delfour.see) | Runnable Symbolic English example. | [`output/delfour.see`](../examples/output/delfour.see) |
| [`deontic-logic.see`](../examples/deontic-logic.see) | Runnable Symbolic English example. | [`output/deontic-logic.see`](../examples/output/deontic-logic.see) |
| [`derived-backward-rule.see`](../examples/derived-backward-rule.see) | Runnable Symbolic English example. | [`output/derived-backward-rule.see`](../examples/output/derived-backward-rule.see) |
| [`derived-rule.see`](../examples/derived-rule.see) | Runnable Symbolic English example. | [`output/derived-rule.see`](../examples/output/derived-rule.see) |
| [`diamond-property.see`](../examples/diamond-property.see) | Runnable Symbolic English example. | [`output/diamond-property.see`](../examples/output/diamond-property.see) |
| [`dijkstra.see`](../examples/dijkstra.see) | Runnable Symbolic English example. | [`output/dijkstra.see`](../examples/output/dijkstra.see) |
| [`dijkstra-findall-sort.see`](../examples/dijkstra-findall-sort.see) | Runnable Symbolic English example. | [`output/dijkstra-findall-sort.see`](../examples/output/dijkstra-findall-sort.see) |
| [`dijkstra-risk-path.see`](../examples/dijkstra-risk-path.see) | Runnable Symbolic English example. | [`output/dijkstra-risk-path.see`](../examples/output/dijkstra-risk-path.see) |
| [`dining-philosophers.see`](../examples/dining-philosophers.see) | Runnable Symbolic English example. | [`output/dining-philosophers.see`](../examples/output/dining-philosophers.see) |
| [`dog.see`](../examples/dog.see) | Runnable Symbolic English example. | [`output/dog.see`](../examples/output/dog.see) |
| [`dpv-odrl-purpose-mapping.see`](../examples/dpv-odrl-purpose-mapping.see) | Runnable Symbolic English example. | [`output/dpv-odrl-purpose-mapping.see`](../examples/output/dpv-odrl-purpose-mapping.see) |
| [`drone-corridor-planner.see`](../examples/drone-corridor-planner.see) | Runnable Symbolic English example. | [`output/drone-corridor-planner.see`](../examples/output/drone-corridor-planner.see) |
| [`easter-computus.see`](../examples/easter-computus.see) | Runnable Symbolic English example. | [`output/easter-computus.see`](../examples/output/easter-computus.see) |
| [`electrical-rc-filter.see`](../examples/electrical-rc-filter.see) | Runnable Symbolic English example. | [`output/electrical-rc-filter.see`](../examples/output/electrical-rc-filter.see) |
| [`epidemic-policy.see`](../examples/epidemic-policy.see) | Runnable Symbolic English example. | [`output/epidemic-policy.see`](../examples/output/epidemic-policy.see) |
| [`equality-saturation.see`](../examples/equality-saturation.see) | Runnable Symbolic English example. | [`output/equality-saturation.see`](../examples/output/equality-saturation.see) |
| [`equivalence-classes-overlap-implies-same-class.see`](../examples/equivalence-classes-overlap-implies-same-class.see) | Runnable Symbolic English example. | [`output/equivalence-classes-overlap-implies-same-class.see`](../examples/output/equivalence-classes-overlap-implies-same-class.see) |
| [`eulerian-path.see`](../examples/eulerian-path.see) | Runnable Symbolic English example. | [`output/eulerian-path.see`](../examples/output/eulerian-path.see) |
| [`ev-range-worlds.see`](../examples/ev-range-worlds.see) | Runnable Symbolic English example. | [`output/ev-range-worlds.see`](../examples/output/ev-range-worlds.see) |
| [`existential-rule.see`](../examples/existential-rule.see) | Runnable Symbolic English example. | [`output/existential-rule.see`](../examples/output/existential-rule.see) |
| [`exoplanet-validation-worlds.see`](../examples/exoplanet-validation-worlds.see) | Runnable Symbolic English example. | [`output/exoplanet-validation-worlds.see`](../examples/output/exoplanet-validation-worlds.see) |
| [`expression-eval.see`](../examples/expression-eval.see) | Runnable Symbolic English example. | [`output/expression-eval.see`](../examples/output/expression-eval.see) |
| [`family-cousins.see`](../examples/family-cousins.see) | Runnable Symbolic English example. | [`output/family-cousins.see`](../examples/output/family-cousins.see) |
| [`fastpow.see`](../examples/fastpow.see) | Runnable Symbolic English example. | [`output/fastpow.see`](../examples/output/fastpow.see) |
| [`fft8-numeric.see`](../examples/fft8-numeric.see) | Runnable Symbolic English example. | [`output/fft8-numeric.see`](../examples/output/fft8-numeric.see) |
| [`fibonacci.see`](../examples/fibonacci.see) | Runnable Symbolic English example. | [`output/fibonacci.see`](../examples/output/fibonacci.see) |
| [`field-nitrogen-balance.see`](../examples/field-nitrogen-balance.see) | Runnable Symbolic English example. | [`output/field-nitrogen-balance.see`](../examples/output/field-nitrogen-balance.see) |
| [`flandor.see`](../examples/flandor.see) | Runnable Symbolic English example. | [`output/flandor.see`](../examples/output/flandor.see) |
| [`floating-point.see`](../examples/floating-point.see) | Runnable Symbolic English example. | [`output/floating-point.see`](../examples/output/floating-point.see) |
| [`four-color-map.see`](../examples/four-color-map.see) | Runnable Symbolic English example. | [`output/four-color-map.see`](../examples/output/four-color-map.see) |
| [`fundamental-theorem-arithmetic.see`](../examples/fundamental-theorem-arithmetic.see) | Runnable Symbolic English example. | [`output/fundamental-theorem-arithmetic.see`](../examples/output/fundamental-theorem-arithmetic.see) |
| [`gd-step-certified.see`](../examples/gd-step-certified.see) | Runnable Symbolic English example. | [`output/gd-step-certified.see`](../examples/output/gd-step-certified.see) |
| [`gdpr-compliance.see`](../examples/gdpr-compliance.see) | Runnable Symbolic English example. | [`output/gdpr-compliance.see`](../examples/output/gdpr-compliance.see) |
| [`good-cobbler.see`](../examples/good-cobbler.see) | Runnable Symbolic English example. | [`output/good-cobbler.see`](../examples/output/good-cobbler.see) |
| [`gps.see`](../examples/gps.see) | Runnable Symbolic English example. | [`output/gps.see`](../examples/output/gps.see) |
| [`graph.see`](../examples/graph.see) | Runnable Symbolic English example. | [`output/graph.see`](../examples/output/graph.see) |
| [`graph-reachability.see`](../examples/graph-reachability.see) | Runnable Symbolic English example. | [`output/graph-reachability.see`](../examples/output/graph-reachability.see) |
| [`gray-code-counter.see`](../examples/gray-code-counter.see) | Runnable Symbolic English example. | [`output/gray-code-counter.see`](../examples/output/gray-code-counter.see) |
| [`greatest-lower-bound-uniqueness.see`](../examples/greatest-lower-bound-uniqueness.see) | Runnable Symbolic English example. | [`output/greatest-lower-bound-uniqueness.see`](../examples/output/greatest-lower-bound-uniqueness.see) |
| [`group-inverse-uniqueness.see`](../examples/group-inverse-uniqueness.see) | Runnable Symbolic English example. | [`output/group-inverse-uniqueness.see`](../examples/output/group-inverse-uniqueness.see) |
| [`hamiltonian-path.see`](../examples/hamiltonian-path.see) | Runnable Symbolic English example. | [`output/hamiltonian-path.see`](../examples/output/hamiltonian-path.see) |
| [`hamming-code.see`](../examples/hamming-code.see) | Runnable Symbolic English example. | [`output/hamming-code.see`](../examples/output/hamming-code.see) |
| [`hanoi.see`](../examples/hanoi.see) | Runnable Symbolic English example. | [`output/hanoi.see`](../examples/output/hanoi.see) |
| [`heat-loss.see`](../examples/heat-loss.see) | Runnable Symbolic English example. | [`output/heat-loss.see`](../examples/output/heat-loss.see) |
| [`herbrand-witnesses.see`](../examples/herbrand-witnesses.see) | Runnable Symbolic English example. | [`output/herbrand-witnesses.see`](../examples/output/herbrand-witnesses.see) |
| [`heron-theorem.see`](../examples/heron-theorem.see) | Runnable Symbolic English example. | [`output/heron-theorem.see`](../examples/output/heron-theorem.see) |
| [`ideal-gas-law.see`](../examples/ideal-gas-law.see) | Runnable Symbolic English example. | [`output/ideal-gas-law.see`](../examples/output/ideal-gas-law.see) |
| [`illegitimate-reasoning.see`](../examples/illegitimate-reasoning.see) | Runnable Symbolic English example. | [`output/illegitimate-reasoning.see`](../examples/output/illegitimate-reasoning.see) |
| [`integer-partitions.see`](../examples/integer-partitions.see) | Runnable Symbolic English example. | [`output/integer-partitions.see`](../examples/output/integer-partitions.see) |
| [`intuitionistic-logic-kripke.see`](../examples/intuitionistic-logic-kripke.see) | Runnable Symbolic English example. | [`output/intuitionistic-logic-kripke.see`](../examples/output/intuitionistic-logic-kripke.see) |
| [`job-shop-scheduling.see`](../examples/job-shop-scheduling.see) | Runnable Symbolic English example. | [`output/job-shop-scheduling.see`](../examples/output/job-shop-scheduling.see) |
| [`knapsack-optimization.see`](../examples/knapsack-optimization.see) | Runnable Symbolic English example. | [`output/knapsack-optimization.see`](../examples/output/knapsack-optimization.see) |
| [`knowledge-engineering-alignment-flow.see`](../examples/knowledge-engineering-alignment-flow.see) | Runnable Symbolic English example. | [`output/knowledge-engineering-alignment-flow.see`](../examples/output/knowledge-engineering-alignment-flow.see) |
| [`knuth-bendix-completion.see`](../examples/knuth-bendix-completion.see) | Runnable Symbolic English example. | [`output/knuth-bendix-completion.see`](../examples/output/knuth-bendix-completion.see) |
| [`language.see`](../examples/language.see) | Runnable Symbolic English example. | [`output/language.see`](../examples/output/language.see) |
| [`law-of-cosines.see`](../examples/law-of-cosines.see) | Runnable Symbolic English example. | [`output/law-of-cosines.see`](../examples/output/law-of-cosines.see) |
| [`least-squares-regression.see`](../examples/least-squares-regression.see) | Runnable Symbolic English example. | [`output/least-squares-regression.see`](../examples/output/least-squares-regression.see) |
| [`linear-logic-resources.see`](../examples/linear-logic-resources.see) | Runnable Symbolic English example. | [`output/linear-logic-resources.see`](../examples/output/linear-logic-resources.see) |
| [`list-collection.see`](../examples/list-collection.see) | Runnable Symbolic English example. | [`output/list-collection.see`](../examples/output/list-collection.see) |
| [`lldm.see`](../examples/lldm.see) | Runnable Symbolic English example. | [`output/lldm.see`](../examples/output/lldm.see) |
| [`manufacturing-quality-control.see`](../examples/manufacturing-quality-control.see) | Runnable Symbolic English example. | [`output/manufacturing-quality-control.see`](../examples/output/manufacturing-quality-control.see) |
| [`map-four-color-search.see`](../examples/map-four-color-search.see) | Runnable Symbolic English example. | [`output/map-four-color-search.see`](../examples/output/map-four-color-search.see) |
| [`markov-logic-network.see`](../examples/markov-logic-network.see) | Runnable Symbolic English example. | [`output/markov-logic-network.see`](../examples/output/markov-logic-network.see) |
| [`matrix-chain-order.see`](../examples/matrix-chain-order.see) | Runnable Symbolic English example. | [`output/matrix-chain-order.see`](../examples/output/matrix-chain-order.see) |
| [`matrix-noncommutativity.see`](../examples/matrix-noncommutativity.see) | Runnable Symbolic English example. | [`output/matrix-noncommutativity.see`](../examples/output/matrix-noncommutativity.see) |
| [`microgrid-dispatch.see`](../examples/microgrid-dispatch.see) | Runnable Symbolic English example. | [`output/microgrid-dispatch.see`](../examples/output/microgrid-dispatch.see) |
| [`missionaries-cannibals.see`](../examples/missionaries-cannibals.see) | Runnable Symbolic English example. | [`output/missionaries-cannibals.see`](../examples/output/missionaries-cannibals.see) |
| [`modal-logic-kripke.see`](../examples/modal-logic-kripke.see) | Runnable Symbolic English example. | [`output/modal-logic-kripke.see`](../examples/output/modal-logic-kripke.see) |
| [`modular-exponentiation.see`](../examples/modular-exponentiation.see) | Runnable Symbolic English example. | [`output/modular-exponentiation.see`](../examples/output/modular-exponentiation.see) |
| [`monkey-bananas.see`](../examples/monkey-bananas.see) | Runnable Symbolic English example. | [`output/monkey-bananas.see`](../examples/output/monkey-bananas.see) |
| [`n-queens-8.see`](../examples/n-queens-8.see) | Runnable Symbolic English example. | [`output/n-queens-8.see`](../examples/output/n-queens-8.see) |
| [`network-sla.see`](../examples/network-sla.see) | Runnable Symbolic English example. | [`output/network-sla.see`](../examples/output/network-sla.see) |
| [`newton-raphson.see`](../examples/newton-raphson.see) | Runnable Symbolic English example. | [`output/newton-raphson.see`](../examples/output/newton-raphson.see) |
| [`nixon-diamond.see`](../examples/nixon-diamond.see) | Runnable Symbolic English example. | [`output/nixon-diamond.see`](../examples/output/nixon-diamond.see) |
| [`observability-log-correlation.see`](../examples/observability-log-correlation.see) | Runnable Symbolic English example. | [`output/observability-log-correlation.see`](../examples/output/observability-log-correlation.see) |
| [`odrl-dpv-fpv-trust-flow.see`](../examples/odrl-dpv-fpv-trust-flow.see) | Runnable Symbolic English example. | [`output/odrl-dpv-fpv-trust-flow.see`](../examples/output/odrl-dpv-fpv-trust-flow.see) |
| [`odrl-dpv-healthcare-risk-ranked.see`](../examples/odrl-dpv-healthcare-risk-ranked.see) | Runnable Symbolic English example. | [`output/odrl-dpv-healthcare-risk-ranked.see`](../examples/output/odrl-dpv-healthcare-risk-ranked.see) |
| [`odrl-dpv-risk-ranked.see`](../examples/odrl-dpv-risk-ranked.see) | Runnable Symbolic English example. | [`output/odrl-dpv-risk-ranked.see`](../examples/output/odrl-dpv-risk-ranked.see) |
| [`orbital-transfer-design.see`](../examples/orbital-transfer-design.see) | Runnable Symbolic English example. | [`output/orbital-transfer-design.see`](../examples/output/orbital-transfer-design.see) |
| [`partial-evaluator.see`](../examples/partial-evaluator.see) | Runnable Symbolic English example. | [`output/partial-evaluator.see`](../examples/output/partial-evaluator.see) |
| [`path-discovery.see`](../examples/path-discovery.see) | Runnable Symbolic English example. | [`output/path-discovery.see`](../examples/output/path-discovery.see) |
| [`peano-arithmetic.see`](../examples/peano-arithmetic.see) | Runnable Symbolic English example. | [`output/peano-arithmetic.see`](../examples/output/peano-arithmetic.see) |
| [`peano-calculus.see`](../examples/peano-calculus.see) | Runnable Symbolic English example. | [`output/peano-calculus.see`](../examples/output/peano-calculus.see) |
| [`peasant.see`](../examples/peasant.see) | Runnable Symbolic English example. | [`output/peasant.see`](../examples/output/peasant.see) |
| [`pell-equation.see`](../examples/pell-equation.see) | Runnable Symbolic English example. | [`output/pell-equation.see`](../examples/output/pell-equation.see) |
| [`pendulum-period.see`](../examples/pendulum-period.see) | Runnable Symbolic English example. | [`output/pendulum-period.see`](../examples/output/pendulum-period.see) |
| [`pointer-analysis.see`](../examples/pointer-analysis.see) | Runnable Symbolic English example. | [`output/pointer-analysis.see`](../examples/output/pointer-analysis.see) |
| [`polynomial.see`](../examples/polynomial.see) | Runnable Symbolic English example. | [`output/polynomial.see`](../examples/output/polynomial.see) |
| [`prime-range.see`](../examples/prime-range.see) | Runnable Symbolic English example. | [`output/prime-range.see`](../examples/output/prime-range.see) |
| [`proof-contrapositive.see`](../examples/proof-contrapositive.see) | Runnable Symbolic English example. | [`output/proof-contrapositive.see`](../examples/output/proof-contrapositive.see) |
| [`quadratic-formula.see`](../examples/quadratic-formula.see) | Runnable Symbolic English example. | [`output/quadratic-formula.see`](../examples/output/quadratic-formula.see) |
| [`radioactive-decay.see`](../examples/radioactive-decay.see) | Runnable Symbolic English example. | [`output/radioactive-decay.see`](../examples/output/radioactive-decay.see) |
| [`register-allocation.see`](../examples/register-allocation.see) | Runnable Symbolic English example. | [`output/register-allocation.see`](../examples/output/register-allocation.see) |
| [`reusable-builtins.see`](../examples/reusable-builtins.see) | Runnable Symbolic English example. | [`output/reusable-builtins.see`](../examples/output/reusable-builtins.see) |
| [`riemann-hypothesis.see`](../examples/riemann-hypothesis.see) | Runnable Symbolic English example. | [`output/riemann-hypothesis.see`](../examples/output/riemann-hypothesis.see) |
| [`route-planning.see`](../examples/route-planning.see) | Runnable Symbolic English example. | [`output/route-planning.see`](../examples/output/route-planning.see) |
| [`sat-solver-dpll.see`](../examples/sat-solver-dpll.see) | Runnable Symbolic English example. | [`output/sat-solver-dpll.see`](../examples/output/sat-solver-dpll.see) |
| [`security-incident-correlation.see`](../examples/security-incident-correlation.see) | Runnable Symbolic English example. | [`output/security-incident-correlation.see`](../examples/output/security-incident-correlation.see) |
| [`send-more-money.see`](../examples/send-more-money.see) | Runnable Symbolic English example. | [`output/send-more-money.see`](../examples/output/send-more-money.see) |
| [`service-impact.see`](../examples/service-impact.see) | Runnable Symbolic English example. | [`output/service-impact.see`](../examples/output/service-impact.see) |
| [`shoelace-polygon-area.see`](../examples/shoelace-polygon-area.see) | Runnable Symbolic English example. | [`output/shoelace-polygon-area.see`](../examples/output/shoelace-polygon-area.see) |
| [`sieve.see`](../examples/sieve.see) | Runnable Symbolic English example. | [`output/sieve.see`](../examples/output/sieve.see) |
| [`skolem-functions.see`](../examples/skolem-functions.see) | Runnable Symbolic English example. | [`output/skolem-functions.see`](../examples/output/skolem-functions.see) |
| [`socket-age.see`](../examples/socket-age.see) | Runnable Symbolic English example. | [`output/socket-age.see`](../examples/output/socket-age.see) |
| [`socket-family.see`](../examples/socket-family.see) | Runnable Symbolic English example. | [`output/socket-family.see`](../examples/output/socket-family.see) |
| [`socrates.see`](../examples/socrates.see) | Runnable Symbolic English example. | [`output/socrates.see`](../examples/output/socrates.see) |
| [`stable-marriage.see`](../examples/stable-marriage.see) | Runnable Symbolic English example. | [`output/stable-marriage.see`](../examples/output/stable-marriage.see) |
| [`statistics-summary.see`](../examples/statistics-summary.see) | Runnable Symbolic English example. | [`output/statistics-summary.see`](../examples/output/statistics-summary.see) |
| [`stirling-bell-numbers.see`](../examples/stirling-bell-numbers.see) | Runnable Symbolic English example. | [`output/stirling-bell-numbers.see`](../examples/output/stirling-bell-numbers.see) |
| [`sudoku-4x4.see`](../examples/sudoku-4x4.see) | Runnable Symbolic English example. | [`output/sudoku-4x4.see`](../examples/output/sudoku-4x4.see) |
| [`superdense-coding.see`](../examples/superdense-coding.see) | Runnable Symbolic English example. | [`output/superdense-coding.see`](../examples/output/superdense-coding.see) |
| [`symbolic-derivative.see`](../examples/symbolic-derivative.see) | Runnable Symbolic English example. | [`output/symbolic-derivative.see`](../examples/output/symbolic-derivative.see) |
| [`term-tools.see`](../examples/term-tools.see) | Runnable Symbolic English example. | [`output/term-tools.see`](../examples/output/term-tools.see) |
| [`totient-summatory.see`](../examples/totient-summatory.see) | Runnable Symbolic English example. | [`output/totient-summatory.see`](../examples/output/totient-summatory.see) |
| [`trust-flow-provenance-threshold.see`](../examples/trust-flow-provenance-threshold.see) | Runnable Symbolic English example. | [`output/trust-flow-provenance-threshold.see`](../examples/output/trust-flow-provenance-threshold.see) |
| [`truth-maintenance-system.see`](../examples/truth-maintenance-system.see) | Runnable Symbolic English example. | [`output/truth-maintenance-system.see`](../examples/output/truth-maintenance-system.see) |
| [`turing.see`](../examples/turing.see) | Runnable Symbolic English example. | [`output/turing.see`](../examples/output/turing.see) |
| [`type-inference.see`](../examples/type-inference.see) | Runnable Symbolic English example. | [`output/type-inference.see`](../examples/output/type-inference.see) |
| [`vector-similarity.see`](../examples/vector-similarity.see) | Runnable Symbolic English example. | [`output/vector-similarity.see`](../examples/output/vector-similarity.see) |
| [`vulnerability-impact.see`](../examples/vulnerability-impact.see) | Runnable Symbolic English example. | [`output/vulnerability-impact.see`](../examples/output/vulnerability-impact.see) |
| [`web-names.see`](../examples/web-names.see) | Runnable Symbolic English example. | [`output/web-names.see`](../examples/output/web-names.see) |
| [`weighted-interval-scheduling.see`](../examples/weighted-interval-scheduling.see) | Runnable Symbolic English example. | [`output/weighted-interval-scheduling.see`](../examples/output/weighted-interval-scheduling.see) |
| [`witch.see`](../examples/witch.see) | Runnable Symbolic English example. | [`output/witch.see`](../examples/output/witch.see) |
| [`wolf-goat-cabbage.see`](../examples/wolf-goat-cabbage.see) | Runnable Symbolic English example. | [`output/wolf-goat-cabbage.see`](../examples/output/wolf-goat-cabbage.see) |
| [`workplace-compliance.see`](../examples/workplace-compliance.see) | Runnable Symbolic English example. | [`output/workplace-compliance.see`](../examples/output/workplace-compliance.see) |
| [`zebra.see`](../examples/zebra.see) | Runnable Symbolic English example. | [`output/zebra.see`](../examples/output/zebra.see) |

## Golden outputs, tests, and conformance

Golden answer outputs live in [`examples/output`](../examples/output). `npm run test:see` covers the SEE integration check, conformance cases, regression checks, runnable examples, and proof-output examples. A curated proof-output suite for examples lives in [`examples/proof`](../examples/proof). 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:

```sh
npm run test:see
npm run test:conformance
npm run conformance:report
npm run test:examples
npm run test:regression
```

## Development and release

The package is plain JavaScript. Source lives under [`src`](../src), examples under [`examples`](../examples), and public conformance fixtures under [`test/conformance`](../test/conformance). Run `npm test` before packaging changes.

## Relationship to Eyeling

SEE is the compact Symbolic English-style member of the family. It uses readable statements such as `parent holds for alice and bob` and `ancestor holds for ?x and ?z if parent holds for ?x and ?y and ancestor holds for ?y and ?z`. It is a good fit if the problem is naturally relational, goal-directed, finite, and does not need RDF graph interchange.

## Performance notes

SEE performs goal-directed search with optional tabling declarations such as `table holds for path and 2`. Tabling is useful for recursive dynamic-programming relations, transitive closures, and finite graph search. Use small output relations and `show` declarations to keep materialization focused.

## Implementation limits

SEE intentionally keeps Symbolic English compact. It has no operator syntax, predicate-parenthesis source syntax, final fact dots, cut, modules, dynamic database updates, DCGs, or large standard library. Arity-zero data is written and read back as an atom, such as `nil`. Negation is negation-as-failure through `not/1`. Search is goal-directed and expected to be finite for the selected output goals.