search

ha-mo-we / Racer

Racer is a knowledge representation system that implements a highly optimized tableau calculus for the description logic SRIQ(D).
Other
106 stars 19 forks source link

Debugging logs? Conflict explanations? #20

Open gschadow opened 5 years ago

gschadow commented 5 years ago

Hello again, sorry for always coming in with two shots. As my ontology grows in complexity, I find myself spending more and more time trying to resolve conflicts. Usually they are related to contradictions (unsatisfiability) introduced through some axioms (domain axioms are particularly dangerous.) Trying to figure these out takes a lot of time, in trial and error removing axioms and adding them one by one, simplifying complex terms to the simplest failing test case, all to figure out what is wrong.

Wouldn't it be possible to turn on some excessive logging which one might analyze to find the problem? Would a feature not be possible with the existing internal data structures where at least some information about conflicting entailments could be shown? I realize it may not be possible to point exactly to the source axiom that caused the conflict, but it would already help if one could just see the proximal cause, such as the names of the roles involved in the contradiction.

Is it possible? I might try to hack in the code myself, one thing that makes it a little harder is that I had no problems grabbing the system with quick-lisp, but actually compiling locally from the git download, so that I could turn the debug feature on, etc., I couldn't figure out yet how to do that. System is SBCL but I can use other open source CL systems if it is better supported for compilation. I work in the RACER-USER package in LISP, don't care about racer-toplevel or servers, DIG, DAML, or OWL.

PS: I only deal with TBox (and RBox) reasoning at this time, so ABox explanations wouldn't help me or are not necessary. I am not looking for anything fancy, just some more clue rather than just returning NIL on concept-satisfiable? or check-tbox-coherence.

thanks much, -Gunther

arademaker commented 5 years ago

Hello @gschadow, you may be missing fundamental knowledge about description logics and reasoning methods for DLs. Most DL provers implement the tableaux proof method (I believe that is the case of Racer too), it is a proof by refutation. In Tableaux, explanations are not easy to be obtained since a simple proof starts by change the proof of a subsumption C ⊑ D to the problem of checking SAT of a concept C ⊓ ¬D. Moreover, proofs are exponential in size. You can find more in https://www.amazon.com/exec/obidos/ASIN/0521150116/acmorg-20.

I am not trying to advertise my work, but that is one of the motivations for my Ph.D. thesis:

The natural deduction and sequent calculus deduction systems that I proposed make possible the construction of direct proofs.

gschadow commented 5 years ago

Oi Alexandre, tudo bem? It's funny, I live near you, for a good time I lived near Gavea, isn't that were PUC Rio is also located? Funny because I originate from Germany where all that good RACER stuff (and even CEL) comes from. Anyway ... Thanks for sharing you thesis, I had a look. You know I'm not really looking for full fledged explanations. I don't even need to find out why things don't subsume all that much. To me it would already help to just see what the issue is that a concept isn't satisfiable. Any dump of the error status would probably be able to hint me into the right direction. Some sort of semi-verbose mode. Possibly simply enabling the debug output that's already in the code, that I just don't know how to enable if I'm using the version loaded via quick-lisp.

arademaker commented 5 years ago

Yep, that is funny. We can talk offline if you want. But I still believe that depends on how Racer is implemented, you may not be able to have more information during the proof construction.

gschadow commented 5 years ago

Well, this "forum" here is about RACER, you might be in the position to actually check out the RACER source code yourself. Really all I am asking for is very, very simple.

When RACER finds that the conjunction of the antecedent and consequent of an implication is not satisfiable -- or really any other finding of not satisfiable -- all I would like to see is just some minimal information about the closest role or concept names involved around that contradiction. Just to guide the debugging. I don't need a full explanation.

I think it might be something very easy to dump out actually. In fact, it seems to me that some of this is already in there. I see debug and flag parameters in files like tbox.list, cd-satisfiable.lisp and racer.lisp. Some of that good stuff is commented away, as in 

    (when nil ;*flag*
      (format t "~%testing satisfiability of constraint system:~%")
      (loop for cd-constraint in (append (and state (reverse (solver-state-cd-constraints state)))
                                         (list constraint)) do
            (format t "~A~%" 
                    (if (cd-constraint-negated-p cd-constraint)
                      (predicate-negation (cd-constraint-predicate cd-constraint))
                      (cd-constraint-predicate cd-constraint))))
      (format t "~A~%" pred))

I really wish that debugging and tracing feature was fully left working so I could use it specifically to test a satisfiability that I am investigating right now. This would help so much to just see such. Look at all that output that's already in the source code that I could use if it wasn't commented out!

Dear Ralf, if you are listening, would it be possible not to comment these things out and tell us what switch we can reliably use to get this fine debug output? Thanks.

gschadow commented 5 years ago

I have tried to re-define this function with the when *flag* stuff un-commented back in, and also (defparameter *flag* T) and (defparameter *debug* T) but I don't see this making any difference. I have overridden other things that had the #+:debug stuff and (setf *features* (cons :debug *features*)) and all that good stuff, and still I can't see ant tracing and debug messages. What am I doing wrong?

gschadow commented 5 years ago

When I defined my problematic concept with (equivalent TEST1 ...) and then (get-concept-definition TEST1) suddenly I got a bunch of tracer output. It isn't clear to me yet what it means though. Lots of output ...

ha-mo-we commented 5 years ago

Dear Gunther,

I am trying hard to send answers to all your issues. Let us first have a look at the transitivity and role implication problems, before developing additional cases. We added role implications late, and the code is not tested that much. But let us see.

Best regards, Ralf

On 11. Jul 2019, at 16:24, gschadow notifications@github.com wrote:

Hello again, sorry for always coming in with two shots. As my ontology grows in complexity, I find myself spending more and more time trying to resolve conflicts. Usually they are related to contradictions (unsatisfiability) introduced through some axioms (domain axioms are particularly dangerous.) Trying to figure these out takes a lot of time, in trial and error removing axioms and adding them one by one, simplifying complex terms to the simplest failing test case, all to figure out what is wrong.

Wouldn't it be possible to turn on some excessive logging which one might analyze to find the problem? Would a feature not be possible with the existing internal data structures where at least the two conflicting entailments could be shown. I realize it may not be possible to point exactly to the source axiom that caused the conflict, but it would already help if one could just see the proximal cause, such as the names of the roles involved in the contradiction.

Is it possible? I might try to hack in the code myself, one thing that makes it a little harder is that I had no problems grabbing the system with quick-lisp, but actually compiling locally from the git download, so that I could turn the debug feature on, etc., I couldn't figure out yet how to do that. System is SBCL but I can use other open source CL systems if it is better supported for compilation. I work in the RACER-USER package in LISP, don't care about racer-toplevel or servers, DIG, DAML, or OWL.

thanks much, -Gunther

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/ha-mo-we/Racer/issues/20?email_source=notifications&email_token=AB2476XF7NW7N2KQAKAMT3TP647CBA5CNFSM4IBIG5T2YY3PNVWWK3TUL52HS4DFUVEXG43VMWVGG33NNVSW45C7NFSM4G6UXBBQ, or mute the thread https://github.com/notifications/unsubscribe-auth/AB2476RVOZWE64ZFKOQ2GQTP647CBANCNFSM4IBIG5TQ.

ha-mo-we commented 5 years ago

On 12. Jul 2019, at 16:56, gschadow notifications@github.com wrote:

Well, this "forum" here is about RACER, you might be in the position to actually check out the RACER source code yourself. Really all I am asking for is very, very simple.

When RACER finds that the conjunction of the antecedent and consequent of an implication is not satisfiable, all I would like to see is just some minimal information about the closest role or concept names involved around that contradiction. Just to guide the debugging. I don't need a full explanation.

I think it might be something very easy to dump out actually. In fact, it seems to me that some of this is already in there. I see debug and flag parameters in files like tbox.list, cd-satisfiable.lisp and racer.lisp. Some of that good stuff is commented away, as in

(when nil ;*flag*
  (format t "~%testing satisfiability of constraint system:~%")
  (loop for cd-constraint in (append (and state (reverse (solver-state-cd-constraints state)))
                                     (list constraint)) do
        (format t "~A~%" 
                (if (cd-constraint-negated-p cd-constraint)
                  (predicate-negation (cd-constraint-predicate cd-constraint))
                  (cd-constraint-predicate cd-constraint))))
  (format t "~A~%" pred))

I really wish that debugging and tracing feature was fully left working so I could use it specifically to test a satisfiability that I am investigating right now. This would help so much to just see such. Look at all that output that's already in the source code that I could use if it wasn't commented out!

Dear Ralf, if you are listening, would it be possible not to comment these things out and tell us what switch we can reliably use to get this fine debug output? Thanks.

Dear Gunther,

Racer is based on a tableau calculus as Alexandre said. Thus, in principle, for instance, (concept-subsumes? c d) is reduced to concept-satisfiable? (and (not c) d)). However, in order to achieve the appropriate runtimes there are very many other algorithms exploited due to the information Racer has available at hand in a particular situation. We did some experiments on computing explanations with (check-abox-coherence). If you do not understand why (concept-subsumes? c d) returns nil, say, you can declare an abox with one individual being an instance of (and (not c) d).

(in-package :racer-user)

(in-knowledge-base test)

(implies a b)

(equivalent c (some r b)) (equivalent d (some r a))

(print (concept-subsumes? c d))

(instance i (and (not c) d))

(check-abox-coherence)

;; ----> (NIL ((I (AND D (NOT C))) (:INFERENCE-STEP :ASSERTION (I D) :AXIOM (IMPLIES D (SOME R A)))))

However, the feature is experimental. The problem is that due to syntactic rewriting for optimization reasons the "explanations" are not really understandable. Furthermore, the tableau calculus for computing explanations is much slower. Note that for (concept-subsumes? c d) to return t every possible model of (and (not c) d) is ruled out, and for every clash being found, dependencies to the original axioms etc must be recorded. Dependency tracing is very tricky (and there might be flaws in the code).

Furthermore, I would like to point out that it does not make any sense to try to activate logging output for Racer. For development we needed to record debugging output in a variable and implemented a window debugger specifically for Racer, which provided facilities to interactively unfold recorded debugging output on demand and showed arguments to functions like in a backtrace. The Racer Tracer was implemented with Lispworks Common Lisp. Unfortunately I do not have a Lispworks license any more (old versions of Lispworks do not run under Mojave, and the Lispworks Personal edition does not allow for enough heap to be allocated to even compile Racer). If you have a Lispworks license available, uncomment ;;;; (pushnew :debug features) in racer.asd and recompile. Then check out tracer.lisp, tracer-support.lisp, and tracer-interface.lisp

The Tracer gives you a trace of calls to internal procedures, however. There is no real explanation facility. Some colleagues from Manchester have worked on this. But I am not sure whether you can find something to download that really works.

Best regards, Ralf