T. Janhunen

made the following comments:

Ad Q1.

The correctness of solvers is crucial (can at least be checked on pseudocode-descriptions) - independent answer set verifiers can be introduced.

Ad Q2.

Optimization is always a tradeoff between length of the program $P$ (compact representation) and execution time $T$ needed to solve the program.

Ad Q3.

As for the compact representation: Suitable Lemmas might often help to solve a problem, so the most compact representation is not always the best wrt. $T$.

The relation of $T$ and $P$, i.e. efficiency of different encodings might be highly dependent on different solvers.

Equivalence preserving transformations are and different notions of equivalence are an important point, effects to performance however, are not completely clear.

One possibility would be ``blind" optimizations (e.g. by dropping rules), using equivalence verifiers as recently proposed.

Ad Q3.

As for the proprietary syntax: It would help if suitable translations should be provided wherever possible.

• normal and disjunctive logic programs now form a safe subset to start with.
• problems might arise if different solvers treat recent syntactic extensions differently.
• Is a low-level format (like DIMACS for SAT-Solvers) achievable?

Ad Q4.

ASP can be implemented in Prolog, but also the following issues might be considered:

• Remote ASP solver calls can be realized in Prolog
• Prolog has problems with negation as failure
• Order of subgoals matters in Prolog
• we should identify common subsets.