Michael Gelfond

made the following statements:

Ad Q1.

For correct programs, start with - empirical evidence - proofs are needed based on precise specifications, e.g. by

(a)

transition diagrams

(b)

electrical circuit viewed as a function from input to output

(c)

inheritance hierarchies based on independently defined semantics

The problem which comes up is here complete vs. incomplete specification.

Ad Q2.

First, one needs a good design. Second, small tricks, which preserve equivalence in some sense (strong, unif., weak). Michael shows two examples:

1. 
      a :- -b.       s      a :- not b.
     -b :- not b.  <===>   -b :- not b.
   
   
2. 
     :- a,b.       add
     :- -a,c.      ===>   :- b,c.
   
   

Ad Q4.

We miss function symbols.