FUB Embedding of propositional production systems into μ- calculus, and first-order production systems into fixpoint logic

From ONTORULE Show Case

A production rule is an expression of the form “if condition-r then action-r”. The intuitive semantics of the rule is: if condition-r holds, then perform action-r. A production system consists of a set of production rules, a working memory, which contains the current state of knowledge, and a rule interpreter, which executes the rules and makes changes in the working memory, based on the actions in the rules. In this work rules in which conditions are first-order logic (FOL) formulas with free variables and the actions are additions and removals of atomic formulas are considered (in addiction to the special case of equality- and variable-free, i.e., propositional, rules); update actions are easily expressible as additions+removals.

Fixpoint operator is exploited in both logics to encode properties of the system over time. One of the advantages of the present encodings is the strong correspondence between the structure of the models and the runs of the production systems, which enables straightforward modeling of properties of the system in the logic.

In addition, it justifies the use of the embedding for further investigation of the systems, as well as future combinations with ontologies. Another possible application of our encodings is the optimization of production systems due to static analysis: One can check, as an example, that a particular rule is never applied, and thus may be discarded. Deciding equivalence of production systems can be reduced to entailment in μ-calculus and FPL. Equivalence can be exploited for optimization by replacing a production system with an equivalent system that is potentially easier to execute.

Corresponding results are reported in Deliverable 3.2.