Gregory M. Kapfhammer

Chapter Ten: Formal Methods (Section 10.4)

• Informally, what is a horn clause? Why does the Prolog language limit first order predicate logic to horn clauses?

Horn clauses express a subset of statements of first-order logic. In first order predicate logic, a horn clause would be written in the form ∃X(answer(kristen, X)∧answer(chris, X)∧answer(jamie, X)∧answer(brian, X)⇒answered(X)). In other words, a horn clause has just one predicate in terms of a conjunction of predicates. A simpler example would be A∧B∧C⇒D. Note that horn clauses cannot make use of the negation symbol.

Prolog limits predicate logic to horn clauses in order to ensure that there is a way to check that the given WFF is true. First order logic is an undecidable system, so by using Horn clauses, Prolog avoids most first-order undecidable questions. For example, there can be no negative requirements in Prolog saying that something does not exists, and there is no universal quantifier.

---

• How can Prolog be used to automatically generate test cases? What are the limits of this approach?

Prolog can be used to write a list of predicates, which can then be used to write the specification. In other words, the input and output behavior of a program is completely defined in the specification. This then gives us an obvious way to generate test cases automatically from the specificiation. The prolog program is its own oracle.

However, the user is the one who has the final say in the correctness of the specification. Two minds can disagree on what's "correct." For example, when sorting a list, if duplicates occur, does the first element that occurs multiple times get placed at the end of the list of the multiple elements in the new list or does it appear first? When tests are made, they still cannot show ultimate correctness; they can only show incorrectness. Prolog also is limited because it cannot express negative requirements or universal specification. Finally, Prolog also experiences a speed issue because it simply starts at the beginning and works until it finds a solution. Thus, a specification can become too slow to be used in practice.

Kristen Walcott and Jamie Ball

---

Links to this Page

• Kristen Walcott last edited on 8 December 2004 at 8:24 pm by acs-24-144-201-80.zoominternet.net
• Requirements Elicitation and Analysis / Specification last edited on 9 December 2004 at 12:07 pm by aldenv28.allegheny.edu