EYE EYE

EYE stands for "Euler Yet another proof Engine" and it is a further
development of Euler which is an inference engine supporting logic
based proofs. EYE is a semibackward reasoning engine enhanced with
Euler path detection.

The Euler path detection is roughly "don't step in your own steps"
to avoid vicious circles so to speak and in that respect there is a
similarity with what Leonhard Euler discovered in 1736 for the
Königsberg Bridge Problem [1].

Semibackward reasoning is pure backward reasoning for backward rules
(rules using <= in N3) and backward-forward-backward reasoning for
forward rules (rules using => in N3).

The backward-forward-backward reasoning is realized via an underlying
Prolog backward chaining, a forward meta-level reasoning and a
backward proof construction.

The reasoning that EYE is performing is grounded in FOL (First Order
Logic). Keeping a language less powerful than FOL is quite reasonable
within an application, but not for the Web [2].


The detailed design of EYE comprises:

1/ N3 [3] parser specified as Prolog DCG (Definite Clause Grammar)

2/ N3Logic [4] to N3P (Notation 3 P-code) [5] compiler

3/ EAM (Euler Abstract Machine) with Euler path detection to avoid loops
   and with postponed brake mechanism to run at much increased speed

4/ proof construction using the vocabulary for proofs [6]

5/ builtins and support predicates for the above functionalities


High performance is crucial and that is the main reason why EYE is
depending on flexible indexing of Prolog clauses during runtime [7].
Indexing Prolog clauses on demand during program execution, also called
JITI (Just In Time Indexing) or DDI (Demand Driven Indexing) can really
make a substantial difference and is in that respect very similar to
indexing used for relational databases. Even a small percentage of
badly indexed calls can end up dominating runtime.

In the current design of EYE things are layered and cascaded as follows:

                     .------------------.
        .------------|- - -   PN3       |
        |       N3P  |-----'------------|
        |------------|- - -'  EAM       |
        |       PVM  |-----'------------|
        |------------|- - -'  WAM       |
        |       ASM  |-----'------------|
        '------------|- - -'  CPU       |
                     '------------------'

	Legend
	------
		PN3	= Programming in Notation 3
		N3P	= Notation 3 P-code
		EAM	= Euler Abstract Machine
		PVM	= Prolog Virtual Machine code
		WAM	= Warren/Wielemaker Abstract Machine
		ASM	= Assembly code
		CPU	= Central Processing Unit


The EYE test cases [8] and their results [9] support the development of EYE.

The usage of EYE via the command line is as follows:

Usage: eye <options>* <data>* <query>*
eye
	swipl -x eye.pvm --
<options>
	--nope			no proof explanation
	--no-qnames		no qnames in output
	--no-distinct		no distinct answers in output
	--single-answer		give only one answer
	--step <count>		set maximimum step count
	--wcache <uri> <file>	to tell that uri is cached as file
	--ignore-syntax-error	do not halt in case of syntax error
	--n3p			output N3 P-code
	--image <file>		output PVM code
	--strings		output log:outputString objects
	--traditional		traditional mode
	--warn			output warning info
	--debug			output debug info
	--debug-cnt		output debug info about counters
	--debug-pvm		output debug info about PVM code
	--rule-histogram	output rule histogram
	--profile		output profile info
	--statistics		output statistics info
	--probe			output speedtest info
	--version		show version info
	--license		show license info
	--help			show help info
<data>
	<n3_resource>		N3 facts and rules
	--turtle <ttl_resource>	Turtle data
	--plugin <n3p_resource>	plugin N3 P-code
<query>
	--query <n3_resource>	output filtered with filter rules
	--pass			output deductive closure
	--pass-all		output deductive closure plus rules
	--pass-only-new		output only the new derived triples


References
----------

 [1] http://mathworld.wolfram.com/KoenigsbergBridgeProblem.html
 [2] http://www.w3.org/DesignIssues/Logic
 [3] http://www.w3.org/TeamSubmission/n3/
 [4] http://www.w3.org/DesignIssues/N3Logic
 [5] http://eulersharp.sourceforge.net/GUIDE
 [6] http://www.w3.org/2000/10/swap/reason
 [7] http://user.it.uu.se/~kostis/Papers/iclp07.pdf
 [8] http://eulersharp.sourceforge.net/2006/02swap/etc.sh
 [9] http://eulersharp.sourceforge.net/2006/02swap/etc.n3