doc.txt

"Equilibrium evaluation for Multi Context Systems in dlvhex" (Praktikum)

=Theoretical Foundations=

Multi Context Systems (MCS) are systems consisting of contexts and rules between
those contexts. A context is a logic with some knowledge base and a semantic
function ACC. ACC decides if the context "accepts" some beliefs, given a certain
knowledge base. Bridge rules are activated by accepted beliefs and add facts to
knowledge bases.

The semantics of MCS are defined as Equilibria - a stable state of belief sets
at each context.

=Programming Objective=

To implement a dlvhex-Plugin which allows to calculate Equilibrium-semantics of
MCS in dlvhex. This Plugin shall provide an generic interface to implement
arbitrary contexts, as well as a possibility to use ASP programs as contexts.

=Implementation Idea=

* An Input file for MCS description is written by the user and contains
  - Bridge Rules: "(1:a) :- (2:bcd), (3:e), not (1:b)."
  - Context descriptions of the form '#context(<num>,<extatom>,<param>).'
    e.g. for ASP contexts: '#context(2,dlv_asp_context_acc,"ctx.dlv").'
      -> uses dlv and program "ctx.dlv" to implement context 2's semantics
    e.g. for User-implemented contexts: '#context(3,foo_context_acc,"parameter").'
      -> uses the external atom "foo_context_acc" to implement context 3's
         semantics (the user will have to implement this atom)
* The Rewrite Plugin (to be written in the Praktikum) parses this input file and
  creates a HEX program which does the following (a detailed description of this
  program exists):
  - guess "Output Beliefs" (= beliefs which are used in bridge rule bodies)
  - evaluate bridge rules (using guessed beliefs as input)
  - check if all contexts accept a belief set which coincides with the guessed
    output beliefs
* The context semantics are evaluated in External Atoms:
  - Implementation of "GenericContext" class in the Praktikum, which contains a
    pure virtual function
    "virtual set<string> acc(const string& param, const set<string>& input) = 0".
    User-implemented HEX atoms look like "&foo_context_acc[in,out,verify,param]()"
    (in, out, verify correspond to lists) and returns 1 iff
    "acc(input) \cap output = verify"
  - Implementation of an external atom in the Praktikum, which is specifically
    suited to evaluate ASP context semantics. The HEX atom looks like
    "&dlv_asp_context_acc[input,output,verify,param]()" and
    calls the "dlv" ASP solver on the program given via param + inputs + simple
    constraints, which enforce the output/verify conditions.
    The Atom returns 1 iff the called solver has an answer set.
    This is more efficient than the GenericContext, but it is only useable for
    ASP contexts. Classes for calling the solver and parsing the result already
    exist in dlvhex and need not be written in the Praktikum.

=Important Additional Requirements=

* SVN on sourceforge will be used to manage the source code. Commits should be
  done often and early, this means we can see problems earlier, react faster,
  and save time both of advisor and student.
* Sourcecode Documentation (comments) is required, so other people can later
  understand and extend the work.
* Testcases shall be written, so that most functionality can automatically be
  verified a bit by nightly builds. This also makes development easier and more
  comfortable (autotools with 'make distcheck' are already used in dlvhex).

=First Steps and General Plan=

* Checkout dlvhex from sourceforge (do NOT download the package, it is some
  years old and does not compile).
* Download/build boost 1.37 or later if you don't have it.
* Build dlvhex and the stringplugin and see how the build system and dlvhex
  works by playing around a bit.
* Write a small concept and a plan (maybe already including detailed syntax,
  some header files, some testcases).
* Meeting about the concept and plan for next steps.
* Write parser, rewriter, generic context atoms, ASP contexts, and test it all
  using at least two derived generic context and two ASP
  contexts.

vim:tw=80:nocindent: