eyedia

Terms

Web data, quoted statements and placeholder names, without any new syntax.

terms.pl · output · proof · check · try it in the playground

---

The question

Data on the web (the Semantic Web, RDF) is made of small statements called triples: subject – predicate – object, such as “this page – has title – hello”. Names are web addresses (IRIs), and text can carry a language tag (“hello”, in English).

Sometimes you also want to talk about a group of statements without claiming they are true — a quoted graph, like quoting someone’s words.

Can a small rule language handle all this without special features?

---

What we tell Eyedia: the data

Everything is written as ordinary nested terms:

quoted(graph([triple(iri('https://example.org/s'), iri('https://example.org/p'), literal('hello', lang(en)))] )).

Read from the inside out:

• iri(...) — a web address used as a name;
• literal('hello', lang(en)) — the text “hello”, tagged as English;
• triple(S, P, O) — one statement;
• graph([...]) — a list of statements, held as a quotation.

---

What we tell Eyedia: the rules

member_of(X, [X|_]).
member_of(X, [_|Xs]) :- member_of(X, Xs).
includes(graph(Triples), Triple) :- member_of(Triple, Triples).
found(T) :+ quoted(G), includes(G, T).
witness(X, W) :+ quoted(X).

• member_of finds an item in a list; includes looks inside a graph.
• found lists every triple inside the quoted graph.
• witness has a W that the rule never fills in. More on that below.

---

What Eyedia concludes

found(triple(iri('https://example.org/s'), iri('https://example.org/p'), literal(hello, lang(en)))).
witness(graph([triple(iri('https://example.org/s'), iri('https://example.org/p'), literal(hello, lang(en)))]), sk_0).

• The one triple inside the quotation has been found.
• In the witness, the unknown W became sk_0: a placeholder name meaning “something exists here”. Eyedia invents such names when a conclusion mentions something the rule never pinned down, and keeps them stable from run to run.

---

Why: the proof in plain words

For found:

1. The quoted graph is a fact we gave — fact 1.
2. The triple is the first item of the graph’s list — the first member_of line, with the rest of the list empty.
3. So the graph includes that triple — the includes rule.
4. So the triple is found — the found rule, with G the graph and T the triple.

For witness: the quoted graph exists (fact 1), so the witness rule fires with X the graph and W = sk_0.

---

Checked, not just claimed

• 5 steps for 2 answers, all 5 verified as exact instances of the program lines they cite.
• No calculations to recompute, no circular reasoning, nothing extra.
• 0 steps taken on trust.

Verdict: checked.

A quoted graph is just data: its triple is found, not asserted as true.

---

Try it

node bin/eyedia.js examples/terms.pl            # the answers
node bin/eyedia.js --proof examples/terms.pl    # with their proof

Or open it in the playground. Add a second triple to the list, for example triple(iri('https://example.org/s'), iri('https://example.org/p'), literal('hallo', lang(nl))), and run again: two found lines appear, one for “hello” in English and one for “hallo” in Dutch.

---

Takeaway

Web addresses, language-tagged text, statements and quotations all fit into plain terms, so the same simple, checkable reasoning works on them.

This site is open source. Improve this page.