eyeon

A symbolic logic programming language implementing a subset of Prolog, with .pl programs, query explanations, executable checks, and independently checked proof certificates.

Start with the hands-on tutorial.

Hello, Socrates

human(socrates).
mortal(Person) :- human(Person).

% Answer
?- mortal(Who).
% Reason
?- why.
% Check
:- assertion(mortal(socrates)).

Run with Node.js 18 or later; no packages to install:

node eyeon.js examples/socrates.pl

The answer is Who = socrates.. why explains the supporting facts and rules; the assertion checks the result. This is ARC: Answer, Reason, Check.

The Reason section is a proof certificate. Check includes its independent verification report alongside the assertions. Negation and collection completeness remain explicit obligations. See the proof specification.

Playground

Open the playground, choose an example, and press Run program. Edit, share, or save your program and its complete answers, proof certificate, and checks.

The subset of Prolog

See the specification for syntax, semantics, and limits.