@INPROCEEDINGS{Basin93d,
AUTHOR        = "David Basin",
TITLE         = "IsaWhelk: Whelk Interpreted in Isabelle",
BOOKTITLE     = "11th International Conference on Logic Programming (ICLP94)",
YEAR          = {1994},
NOTE          = {Paper is full version of conference abstract},
ABSTRACT      = {
The Whelk logic has been proposed as a foundation for
logic program synthesis. Here, I interpret the rules of
Whelk as rules of first-order logic and derive them in Isabelle.
Theoretically, this provides a means to understand the meta-theory
behind Whelk, and its correctness.  The interpretation
suggests simplifications, corrections, and extensions. Practically,
it provides a way to construct logic programs from proofs
of their correctness by applying the formalized proof rules
using higher-order resolution. },
}