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!