Available demos:
+-The logical language features functions and equality, first-order quantification, standard names, and sorts. -(Predicates are not built-in but can be simulated with no overhead using boolean functions.) -Knowledge bases are restricted to be in clausal form with only universally quantified variables – these KBs are called proper+. -(Existentially quantified variables in the knowledge base can be simulated with functions.) -Queries are not subject to any syntactic restriction. +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:
+-Decision procedures for sound entailment [KR-2016] and sound consistency [ECAI-2016] are implemented, including conditional beliefs [ECAI-2016] and introspection [IJCAI-2013]. -Adding situation calculus-style actions [KR-2014] is future work. +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.
-The reasoner is written in C++. -The code is available at github.com/schwering/lela. -This demo is compiled to Javascript by emscripten. -As a rule of thumb, the execution time of the Javascript is about 200%–400% of the comparable native binary on my computer—this varies however depending on the browser or Javascript engine and the demo. +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.
-Please report bugs to c.schwering@unsw.edu.au. +The language furthermore comprises conditional belief to refer to differently plausible beliefs. +For instance, we could write B 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. +