From Functional Specifications to Logic Programs
Michael Gelfond, Alfredo Gabaldon · The MIT Press eBooks · 1997
The paper investigates a methodology for representing knowledge in logic programming using functional specifications. The methodology is illustrated by an example formalizing several forms of inheritance reasoning. We also introduce and study a new specification constructor which corresponds to removal of the closed world assumption from input predicates of functional specifications. 1 Introduction "The only effective way to raise the confidence level of a program significantly is to give a proof of its correctness. But one should not first make the program and then prove its correctness, because then the requirement of providing the proof would only increase the poor programmer's burden. On the contrary: the programmer should let correctness proof and program grow hand in hand. ...If one first asks oneself what the structure of a convincing proof would be and, having found this, then construct a program satisfying this proof's requirements, then these correctness concerns turn out to...