FAQ

Q: How to set up the build environment?
   How are RDF/XML files handled?
   How to run the test cases?

A: See http://eulersharp.sourceforge.net/README


Q: Why does <eg:a> <rdf:type> <eg:b> fail?

A: The reason is that <rdf:type> is a URI, using *scheme* rdf
   and you should use rdf:type instead which is a Qname using
   rdf: *namspace prefix*.
   Things like <eg:a> should actually be written as eg:a
   i.e. you either write <http://example.org/xyz#a> or eg:a.


Q: Is the Euler path detection a valid mechanism?

A: We believe that following holds for the Euler path detection 
   Solution Lemma II:
   Be C the set of all closure paths that generate solutions,
   then there exist matching resolution paths that generate
   the same solutions. 
   (or no solutions are excluded) and 
   Infinite Looping Path Lemma:
   If the closure graph G' is not infinite and the resolution 
   process generates an infinite number of looping paths then
   this generation will be stopped by the anti-looping technique
   and the resolution process will terminate in a finite time.

   For more explanation see Master thesis of Guido Naudts
   http://www.agfa.com/w3c/2002/02/thesis/thesis.pdf
   which is about RDFEngine using same anti-looping technique:
   Chapter 5
   [[
   5.14. Anti-looping technique .......................... 94
   5.14.1. Introduction .................................. 95
   5.14.2. Elaboration ................................... 95
   5.14.3. Failure ....................................... 97
   5.14.4. Soundness and completeness .................... 97
   5.14.5. Monotonicity .................................. 97
   ]]
   and Appendix 5
   [[
   5.3. Lemmas .......................................... 151
   ]]


Q: What reasoning technique is Euler using? Is it using Tableaux?

A: No tableaux but resolution (Robinson 1965).
   Euler(sharp) is a backward-chaining reasoner enhanced
   with Euler path detection and will tell you whether a
   given set of facts and rules supports a given conclusion.
   (the latter as an N3 expression obtained by some
   primitive instrumentation of the code).

   For both euler.pl and sem.pl the euler path detection is
   roughly "don't step in your onwn steps" to avoid vicious
   circles so to speak and in that repect there is a similarity
   with what Leonhard Euler discovered in 1736 for the
   "Königsberg Bridge Problem"
   http://mathworld.wolfram.com/KoenigsbergBridgeProblem.html

   Both reasoners are essentially backward-forward-backward
   reasoners i.e. Prolog underlying backward chaining, forward
   meta-level reasoning and backward proof construction.


Q: What are the numbers TC, TP, BC, etc at the last line of
   http://eulersharp.sourceforge.net/2007/07test/shubertE.n3

A: Those are counters keeping track of:
   TC = trunk conclusions
   TP = trunk premises
   BC = branch conclusions
   BP = branch premises
   PM = possible models
   CM = counter models
   FM = false models
   AM = all models