next up previous
Next: Discussion and remarks from Up: Statements of the panelists Previous: T. Janhunen

Hudson Turner

commented as follows.

Ad Q1.
He points out again that the generate and test paradigm is a nice general approach for this direction. Furthermore, Turner's reported about his own experience from using ASP in reasoning about actions.

Proving correctness means proving one to one correspondence between models and solutions.

Theorems like splitting set and generalizations are useful for proving correctness.

For devising translations maybe a few ideas are needed. These ideas should be used as idioms. One example is completeness:

   a :- not -a.
   -a :- not a.
  intertia:
  f1 :- f0, not -f1.
  -f1 :- f0, not f1.

Are these intuitively correct? With these idioms in mind high-level languages work.

Implementations of high-level languages are important to test bigger examples!



Stefan Woltran 2005-08-22