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"
and in that respect there is a similarity with what Leonhard Euler
discovered in 1736 for the Königsberg Bridge Problem [1].
EYE sees the rule P => C as P & NOT(C) => C so it follows so called
PNC steps (PNC stands for "Premis and Not Conclusion").

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:

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

	Legend
	------
		GRE	= Generic Reasoning Engine
		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-numerals		no numerals 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
	--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
	--traditional		traditional mode
	--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