search

own-pt / cl-krr

Environment for knowledge representation, reasoning, and engineering.
Apache License 2.0
4 stars 3 forks source link

Explain why formula can't be translated to TPTP-FOF #19

Open fcbr opened 5 years ago

fcbr commented 5 years ago

It would be great for debugging purposes if we could output why a particular formula isn't eligible to be translated to TPTP/FOF. Basically it would entail changing this code https://github.com/own-pt/cl-krr/blob/master/tptp.lisp#L81-L96 to return a reason instead of just true and false.

arademaker commented 5 years ago

two errors in a recent implementation prevent the generation of fof code without warning:

  1. function not defined (e.g. InList vs. inList)

  2. use of terms in predicate position (e.g. (=> ListFn(...) ...)