Questions from Ontolog

"I have a couple of questions regarding IKL; however, I can only attend the first part of the conference. So it is OK for me to answer them later, but perhaps they are interesting for the conference as well. TillMossakowski (R2Y)

* is there a (complete) calculus for IKL? (R2Z)

A: No. There are (fairly obvious) ND rules for the new constructions, but we have not established completeness yet. This is likely to be quite difficult to do.

* are there tools for IKL (parser, inference engine)?

There is a parser (an easy adaptatation of a KIF parser) but no inference engine as yet, AFAIK.

(R30)
* is it possible to efficiently typechek formulas with an inference engine? (i.e. given that type information is coded via predicates somehow)

A: Along the lines suggested in the IKL Guide, you mean? I think so, but the details have to be worked out. Just dropping type-check axioms into a general inference engine is likely to be prohibitively slow. I am confident that typoe checking can be doen efficiently by a special-purpose inference strategy but the details need to be worked out, and this has not yet been done.

(R31)
* I do not get the point of (that p). In the IKL guide, it is claimed that IKL is compositional. But then, |= (iff p q) implies I(p)=I(q), ...

A:(interruption) No, it does not imply that. It might do so if we were to identify propositions with their extensions, i.e. with truthvalues, but we do not. In fact, CL (on which IKL is based) does not identity any relation with its extension. So for example this is not logically valid in CL:

(if (forall (...)(= (f ...)(g ...))) (= f g))

One observation which may also be relevant. In IKL, the (that <sentence>) construction is part of the basic syntax of the language, and has a meaning defined by the language's semantics. It should not be read as the application of a function called 'that' to a sentence as an argument: the similarity of appearance is merely an accidentail side-effect of the decision to use a LISP-style overall surface syntax.

... which in turn implies I(that p)=I(that q), which implies |= (= (that p) (that q)), which means that there are really only two propositions, namly (that false) and (that true). (R32)

* I do not understand captured names either. On the slides, it is claimed that they map contexts to referents. In the IKL specification, I did not find anything about contexts. I did not find semantic clauses that helped me to interpret ('<string>') either.

A: The slides try to convey the intuition and intended uses. Formally, all that IKL specifies is the no-argument case, i.e that ('name')=name, for any name character string. This is the first condition in the second semantic table of 'extra reference conditions' in the IKL spec. There is no logically required relationship between name and ('name' foo) for any argument foo, but the intended use is where foo denotes a context or informatin source of some kind. In case you are wondering what relation there should be between a context-related name and the same name used without a context argument, the answer is, none. This is what the context logics say, and so we reproduce that in IKL by this construction, whose main logical purpose is to block unwanted equality inferences. Positive conclusions must follow from particular ontological theories of contextual names. The point we claim is that IKL makes it easier to write such theories.