# SEE Language Reference

This document defines the public SEE surface language. SEE stands for **Symbolic English Engine**. Input programs and derived answers use Symbolic English syntax. Compact proof summaries are emitted as ordinary `explanation holds for "..."` SEE facts; optional proof-tree output is human text; full proof-data output is nested SEE data.

## Contents

1. [Overview](#overview)
2. [Source text](#source-text)
3. [Statements](#statements)
4. [Terms](#terms)
5. [Variables and atoms](#variables-and-atoms)
6. [Rules and goals](#rules-and-goals)
7. [Lists and nested terms](#lists-and-nested-terms)
8. [Declarations](#declarations)
9. [Standard built-in predicates](#9-standard-built-in-predicates)
10. [Implementation-specific built-ins](#10-implementation-specific-built-ins)
11. [Proof output](#proof-output)
12. [Conformance](#conformance)

## Overview

A SEE program is a sequence of newline-separated Symbolic English statements. A fact states a relation. A rule states a relation that holds if one or more goals hold. A declaration configures output, tabling, modes, or determinism.

```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
```

SEE source does not use predicate parentheses, comma-separated goal lists, final fact dots, or symbolic rule markers. The parser rejects those forms so the public language stays Symbolic English.

## Source text

Statements are separated by newlines. Blank lines are ignored. A `#` starts a line comment outside quoted strings and backtick atoms.

```see
# comment
answer holds for ok if eq holds for ok and ok
```

## Statements

A relation statement writes a name followed by `holds for` and zero or more arguments joined by `and`. A rule adds `if` and one or more goals, also joined by `and`. SEE accepts one surface syntax only: old aliases such as `has`, `when`, and `also` are rejected so programs stay unambiguous.

```see
score holds for case1 and 95
status holds for ?case and accepted if score holds for ?case and ?score and ge holds for ?score and 90
```

## Terms

A term is an atom, number, string, variable, list, or nested compound term. Nested compound terms are written with `the fact that ... end` so argument boundaries remain unambiguous.

```see
payload holds for case1 and the fact that score holds for 95 end
```

## Variables and atoms

Variables begin with `?`, such as `?case`, `?score`, and `?x`. The bare `_` is anonymous. Simple atoms are bare words such as `case1`, `accepted`, and `parent`. Atoms that need punctuation or reserved words can be written with backticks, for example `` `https://schema.org/name` ``.

Strings use double quotes. Numbers use decimal notation.

## Rules and goals

Rule bodies use `and` for conjunction. Built-ins are called exactly like user-defined relations.

```see
accepted holds for ?case if score holds for ?case and ?score and threshold holds for ?threshold and ge holds for ?score and ?threshold
```

## Lists and nested terms

A proper list is written as `empty list` or `list of item and item`. An open list can use `then` for its tail. When a list is used as an argument inside another relation, wrap it with `the` and `end` so the argument boundary is explicit.

```see
items holds for the list of a and b and c end
open_items holds for the list of a and b then ?rest end
```

Nested relation terms use `the fact that` and `end`:

```see
helper holds for case1 and the fact that score holds for 95 end
```

## Declarations

`show facts for name with arity values` selects relations for default CLI output. Other declarations are ordinary SEE statements interpreted by the program loader:

```see
show facts for answer with 2 values
table holds for path and 2
mode holds for path and 2 and the list of in and out end
semidet holds for edge and 2
```

## 9. Standard built-in predicates

The bundled implementation currently registers 80 name/arity entries across 78 predicate names. This section lists the portable relation names and arities. In source, call them with Symbolic English syntax, for example `eq holds for ?left and ?right` for `eq/2`.

| 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. |

## 10. Implementation-specific built-ins

Hosts may add registry entries for domain-specific work. A custom builtin should be documented by name and arity, should use ordinary Symbolic English relation syntax, and should not require new punctuation in source text.

## Proof output

When proof output is enabled with `--proof` or `-p`, each answer is followed by a compact `explanation holds for "..."` fact. The summary names the rule, fact, or builtin that justified the answer, lists direct support predicate signatures, and hides lower proof steps instead of repeating large terms recursively.

```see
answer holds for ok
explanation holds for "because rule example.see:2; uses seed/1 via fact example.see:1"
```

`--proof=tree` prints an indented readable tree and abbreviates long terms and lists. `--proof=full` prints the complete nested SEE proof data using terms such as `the fact that proof holds for ... end`, `the fact that goal holds for ... end`, `the fact that by holds for ... end`, and `the fact that bindings holds for ... end`. Full proof data is useful for tooling, but can be very large for recursive programs.

## Conformance

The public conformance corpus lives under [`test/conformance`](../test/conformance), and the summary report is [`conformance-report.md`](../conformance-report.md). Positive fixtures are parseable SEE programs. Error fixtures are invalid SEE programs used to pin diagnostics. Warning fixtures pin non-fatal diagnostics such as unstratified negation warnings.

### Small examples

```see
show facts for square with 2 values
square holds for ?x and ?y if mul holds for ?x and ?x and ?y
square holds for 3 and ?y if square holds for 3 and ?y
```

```see
show facts for status with 2 values
closed holds for b
open holds for ?x if not holds for the fact that closed holds for ?x end
status holds for a and open if open holds for a
```