All men are mortal. Socrates is a man. Therefore Socrates is mortal. One fact, one rule, one conclusion, and the smallest complete tour of what EyeProlog does: answer, reason, check.
Run it in the playground ยท Source
Is Socrates mortal, and can the program show why?
type(socrates, man).
type(X, mortal) :-
type(X, man).
holds_result(test, true) :-
type(socrates, mortal).
The fact says Socrates is a man. The rule says that anything that is a man is
mortal: X stands for any individual. The last clause turns the conclusion
into a test result.
eyeprolog examples/socrates.pl
type(socrates, mortal).
holds_result(test, true).
The answers are themselves Prolog facts, so they can be saved and loaded into
another program. type(socrates, man) is not printed: it was given, not
derived.
eyeprolog --proof examples/socrates.pl
step(type(socrates, mortal), rule(2), ['X' = socrates], [type(socrates, man)]).
step(type(socrates, man), fact(1), [], []).
step(holds_result(test, true), rule(3), [], [type(socrates, mortal)]).
Socrates is mortal by rule 2 with X = socrates, using the fact that he is a
man (fact 1). Each conclusion gets exactly one step, naming the clause and
the bindings that justify it.
eyeprolog --proof examples/socrates.pl > socrates.why.pl
eyeprolog --check-proof socrates.why.pl examples/socrates.pl
condition('C1', resolution, ok, 3).
condition('C2', well_founded, ok, 3).
condition('C4', coverage, ok, 4).
verdict(checked).
A separate checker replays all 3 steps against the program without searching for anything. It confirms that each step follows from the clause it cites (C1), that nothing rests on itself (C2), and that every claim is covered (C4).
type(plato, man). and predict the new answer.socrates.why.pl so the first step binds 'X' to plato, then check
it again. Which condition fails?type(X, philosopher) :- type(X, man), teaches(X, _). and a teaches/2
fact.Learn more in The Art of EyeProlog, Chapters 1 and 11.