Available demos:
The reasoner uses a first-order modal logic as representation language. In their most basic form, formulas are about the equality of terms—functions, variables, or standard names. For instance, we could say fatherOf(Sally) = x, where fatherOf is a unary function, x is a variable, and Sally is a standard name (it denotes one specific individual). Predicates are not an explicit part of the language, but can be easily simulated with functions and a special standard name T that indicates truth: rich(x) = T would represent the x is in the relation rich. Such literals can be used to form more complex formulas using logical connectives such as logical negation, disjunction/conjunction, and existential/universal quantification. For example, ∃x (fatherOf(Sally) = x ∧ rich(x) = T) means Sally's father is rich. Finally, modal operators allow to expressly refer to what is known or considered possible. These modal operators are indexed with a natural number that indicates how much reasoning effort is put into proving the formula in its scope. A statement such as "I know Sally's father is rich, but I don't know him personally" could be formulised as follows:
The above example is a typical query. As for knowledge bases, we make a syntactic restriction to so-called proper+ formulas: knowledge bases need to be conjunctions of clauses without existential quantifiers. Note that every knowledge base can be brought into proper+ form by converting it into prenex-CNF and Skolemizing the existentialy quantified variables. Furthermore, knowledge bases are assumed have no nested modal operators.
To help the reasoner optimise query evaluation, the user provide a guarantee that the knowledge base is consistent with a special modal operator: G α indicates that when evaluating α, the knowledge base can be assumed to be consistent.
The language furthermore comprises conditional belief to refer to differently plausible beliefs. For instance, we could write Bkl fatherOf(Sally) = Frank ⟹ rich(Frank) = T to say that we believe that if Frank is Sally's father, he most presumably is rich.
Reasoning in this language is fundamentally based on case splitting—that is, by testing all possible denotations of a term like fatherOf(Sally)—and on unit propagation and subsumption. The reasoning procedures are sound with respect to classical first-order logic, but sacrifice completeness for the sake of decidability. This means that whenever Kk α can be inferred from a knowledge base, then K α holds in the classical semantics, that is, α follows from the knowledge base. Analogously, whenever Mk α can be inferred from a knowledge base, then M α holds in the classical semantics, that is, α is consistent with the knowledge base.
The reasoner is implemented in C++ and will be available as open source. This demo is compiled to Javascript by emscripten. As a rule of thumb, the execution of the Javascript takes about 200%–400% of the native binary's execution time—this may however vary depending on the computer, browser or Javascript engine, and the demo.
For future work, we plan to integrate sutation calculus-style actions.