EYE --- EYE stands for "Euler YAP Engine" and it is a further incremental development of Euler which is an inference engine supporting logic based proofs. EYE is a backward-forward-backward chaining reasoner design enhanced with Euler path detection. The backward-forward-backward chaining is realized via an underlying Prolog backward chaining, a forward meta-level reasoning and a backward proof construction. 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]. 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]. Internally EYE is using N3P (Notation 3 P-code) intermediate code. Every FOL theory has a conservative extension that is equivalent to a N3P theory, a result that goes back to Thoralf Skolem who developed Coherent Logic to obtain metamathematical results in lattice theory and projective geometry [3]. EYE supports MONADIC reasoning (MONotonic Abduction-Deduction-Induction Cycle). Monotonicity is a crucial characteristic of FOL and abduction, deduction and induction are taken from what was orginally intended by Peirce according to Flach and Kakas in [4]: "Instead, he identified the three reasoning forms - abduction, deduction and induction - with the three stages of scientific inquiry: hypothesis generation, prediction, and evaluation. The underlying model of scientific inquiry runs as follows. When confronted with a number of observations she seeks to explain, the scientist comes up with an initial hypothesis; then she investigates what other consequences this theory, were it true, would have; and finally she evaluates the extent to which these predicted consequences agree with reality. Peirce calls the first stage, coming up with a hypothesis to explain the initial observations, abduction; predictions are derived from a suggested hypothesis by deduction; and the credibility of that hypothesis is estimated through its predictions by induction." A single EYE reasoning run is MONADIC: the possible hypotheses (abduction) are generated as e:possibleModel graphs; the predictions (deduction) are either generated as a r:gives graph or the possible model becomes a e:counterModel; the reality check (induction) is generated as an e:inductivity triple expressing the ratio possible/(possible+counter) which is playing nice with belief calculus [5]. The detailed design of EYE comprises: 1/ N3 [6] parser specified as Prolog DCG (Definite Clause Grammar) 2/ N3Logic [7] to N3P (Notation 3 P-code) [8] compiler allowing existentials, disjunctions and false in the conclusion of rules 3/ eam/1 engine with Euler path detection to avoid loops and with postponed brake mechanism to run at much increased speed 4/ eam/3 engine with euler path detection to avoid loops and creating possible models, false models and counter models 5/ proof construction using the http://www.w3.org/2000/10/swap/reason vocabulary for proofs 6/ builtins which can be extended via a web based plugin mechanism so that new functionalities can be easily added without a total redesign of the reasoner 7/ 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 [9]. 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. The test cases [10] and their reference results [11] are a major support to guide the test case driven development of EYE. In the current design of EYE things are layered and cascaded as follows: .------------------. .------------|- - - N3S | | N3P |-----'------------| |------------|- - -' EAM | | PVM |-----'------------| |------------|- - -' WAM | | ASM |-----'------------| '------------|- - -' CPU | '------------------' Legend ------ N3S = Notation 3 Socket 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 For proof tactics the main idea is to annotate the original N3 formulae instead of tampering with them. That way proof tactics can even be derived on the fly using N3 rules. Proof tactics can be declared with the binary predicate e:tactic { => } e:tactic ( ). The subject of e:tactic is an instance of => and the object of e:tactic is a list containing and . For every reasoning step there is a which is initially the empty list. Input clauses that have an e:tactic are only selected when their unifies with the and when the input clause can be satisfied becomes . The usage of EYE is either via a Java wrapper [12] or via the command line: Usage: eye * * * eye java -jar Euler.jar [--no-install] [--swipl] [--yap] swipl -q -f euler.yap -g main -- yap -q -f euler.yap -g main -- --nope no proof explanation --no-branch no branch engine --no-blank no blank nodes in output --no-qvars no quantified variables in output --no-qnames no qnames in output --no-span no span control --quiet incomplete e:falseModel explanation --quick-false do not prove all e:falseModel --quick-possible do not prove all e:possibleModel --quick-answer do not prove all answers --think generate e:consistentGives --ances generate e:ancestorModel --wcache to tell that uri is cached as file --tmp-file temporary file used by N3 Socket --wget-path the path followed by wget --ignore-syntax-error do not halt in case of syntax error --image output PVM code --strings output log:outputString objects --warn output warning info --debug output debug info --profile output profile info --statistics output statistics info --version show version info --help show help info n3 facts and rules --query output filtered with filter rules --pass output deductive closure --pass-all output deductive closure plus rules References ---------- [1] http://mathworld.wolfram.com/KoenigsbergBridgeProblem.html [2] http://www.w3.org/DesignIssues/Logic.html [3] http://www.ii.uib.no/acl/description.pdf [4] http://www.cs.bris.ac.uk/~flach/AbdIndBook/secure/PostScript/flach-kakas.ps.gz [5] http://lists.w3.org/Archives/Public/www-archive/2010Nov/0004.html [6] http://www.w3.org/TeamSubmission/n3/ [7] http://www.w3.org/DesignIssues/N3Logic [8] http://eulersharp.sourceforge.net/GUIDE [9] http://user.it.uu.se/~kostis/Papers/iclp07.pdf [10] http://eulersharp.sourceforge.net/2006/02swap/etc [11] http://eulersharp.sourceforge.net/2006/02swap/etc.ref [12] http://eulersharp.sourceforge.net/2004/01swap/docs/java/javadoc/euler/ProofEngine.html