Animation of Horn Clause Proofs
Ken Kahn, Palo Alt · 1992
Janus, a concurrent constraint programming language, provides an efficient and expressive means of constructing distributed and parallel computations [5]. Concurrent logic programming languages [4] are a special case of concurrent constraint programming languages in which the constraint system is confined to the Herbrand domain. Concurrent logic programs are collections of Hom clauses with control annotations. The execution of a terminating concurrent logic program can be viewed as a proof of a query using the program as a set of axioms. The implementations of such languages can be seen as sound but incomplete theorem provers. Pictorial Janus was built to support a pictorial syntax for the Janus programming language [2, 3]. [ 1] explores the ways in which Pictorial Janus, while constructed to visualize concurrent constraint programs and their executions, can be used to automatically produce animated illustrations of proofs. Furthermore, theorems can be stated in terms of diagrams which are automatically proved and animated. The diagrams are capable of expressing Hom clauses with variables and terms. The meaning of such a diagram relies only upon the topological properties of the drawing. Shapes and colors are used to improve readability and aesthetics, but play no semantic role. A component of the Pictoral Janus system is a parser of PostScript descriptions of drawings. Thus, theorem diagrams can be constructed using any illustration tool capable of producing PostScript output. Using only this output, the parser discovers what elements are variables, terms, clauses, and so on. This information, along with the