diff --git a/load.lisp b/load.lisp
index 904bdfeb1cb9834ef36aa3c61de27def67209154..f97b09b477087ad004e19f56f253e98183391468 100644
--- a/load.lisp
+++ b/load.lisp
@@ -7,5 +7,5 @@
              "pvs"))
   (load (concatenate 'string "specs/src/" m ".lisp") ))
 
-(dolist (m '("tptp" "proof-json"))
+(dolist (m '("proof-common" "tptp" "proof-json" "proof-dk"))
   (load (concatenate 'string "proofs/src/" m ".lisp")))
diff --git a/proofs/src/proof-common.lisp b/proofs/src/proof-common.lisp
new file mode 100644
index 0000000000000000000000000000000000000000..f91ea3c508fa661d3d14e8dc74b6a4ed05d4ee13
--- /dev/null
+++ b/proofs/src/proof-common.lisp
@@ -0,0 +1,9 @@
+(in-package :pvs)
+
+(defun pp-path (stream ps &optional colon-p at-sign-p)
+  "Print the path from the top state to proof state PS on stream STREAM."
+  (declare (ignore colon-p at-sign-p))
+  (let ((pth (path-from-top ps)))
+    (if (endp pth)
+        (princ "root" stream)
+        (format stream "~{~a~^.~}" pth))))
diff --git a/proofs/src/proof-dk.lisp b/proofs/src/proof-dk.lisp
new file mode 100644
index 0000000000000000000000000000000000000000..6e20d7b65d5038ceebf2c23e0b6d7d9dd1a67615
--- /dev/null
+++ b/proofs/src/proof-dk.lisp
@@ -0,0 +1,13 @@
+(in-package :pvs)
+
+(defun ps->dk (ps)
+  (with-slots ((goal current-goal) (lab label) (pps parent-proofstate)
+               (ctx context) (crule current-rule)) ps
+    (let* ((name (format nil "{|~a ~/pvs:pp-path/|}" lab ps))
+           (forms (mapcar #'formula (s-forms goal)))
+           (formula (make!-disjunction* forms)))
+      (format t "Translating~%")
+      (format t "symbol ~a: Prf ~:/pvs:pp-dk/;" name formula))))
+
+(pushnew #'ps->dk *proofstate-hooks*)
+(pushnew #'ps->dk *success-proofstate-hooks*)
diff --git a/proofs/src/tptp.lisp b/proofs/src/tptp.lisp
index 53c691d5f6aa1c02ca4ccd58a264e7b1c5534af5..9ca65f8708c8488dc871a479e17ea7a85d1e4f68 100644
--- a/proofs/src/tptp.lisp
+++ b/proofs/src/tptp.lisp
@@ -328,13 +328,6 @@
         (format nil "fof(~a, ~a, ~a, ~a)." name role expr source)
         (format nil "fof(~a, ~a, ~a)." name role expr))))
 
-(defun pp-path (stream ps &optional colon-p at-sign-p)
-  (declare (ignore colon-p at-sign-p))
-  (let ((pth (path-from-top ps)))
-    (if (endp pth)
-        (princ "root" stream)
-        (format stream "~{~a~^.~}" pth))))
-
 (defgeneric pvs->tptp (thing)
   (:documentation "Translate a THING to TPTP"))
 
@@ -361,10 +354,11 @@
   "Take the longest prefix of S without dot."
   (car (excl:split-re "\\." s)))
 
-#+sbcl
+#-allegro
+(require :cl-ppcre)
+#-allegro
 (defun prefix-no-dot (s)
   "Take the longest prefix of S without dot."
-  (require :cl-ppcre)
   (car (cl-ppcre:split "\\." s)))
 
 (defun output-tptp-proofstate-to-stream (ps)