PTTP(Prolog Technology Theorem Prover) in MCL.

[jin@Eagle.MIT.EDU (Jintae Lee)]

PTTP extends the usual prolog in several ways (Mark Stickel, J. 
Automated Reasoning 1988).  And it is written by Mark mostly in pure 
commonlisp except the proof printing part, which is listed below and 
specific to Symbolics.  In order to rewrite this part for MCL, I need 
to know what MCL's counter-parts are of the SCL.  If anybody already 
ported PTTP to MCL or has the relevant knowledge, please let me know.  
Thanks.

BTW if you know of other prolog implementations in common lisp, I 
would appreciate the info. as well.

-jin

#+SYMBOLICS
(scl:defflavor print-proof () (scl:condition))

#+SYMBOLICS
(scl:defmethod (print-proof :report) (stream) nil)

#+SYMBOLICS
(defun print-proof (condition-object)
  (dbg:with-erring-frame (frame-ptr condition-object)
    (let (goals)
      (do ((frame-ptr frame-ptr 
(dbg:frame-previous-interesting-active-frame frame-ptr)))
	  ((null frame-ptr))
	(let* ((l (dbg:get-frame-function-and-args frame-ptr))
	       (n (and (symbolp (car l))
		       (not (invisible-functor-p (car l)))
		       (not (getf (get (car l) 'compiled-parameters) 
:split-procedure))
		       (get (car l) 'arity))))
	  (when n
	    (let ((k (DBG:FRAME-LOCAL-VALUE FRAME-PTR '!NSUBGOALS! T)))
	      ;; Symbolics bug: above results in an error if there is no 
!nsubgoals! variable in the stack frame
	      (push (if k
			(list n l (car k) (cadr k))
			(list n l 0 nil))
		    goals)))))
      (format t "~2&Proof:~%Goal#  Wff#  Wff Instance~%-----  ----  
------------")
      (print-proof1 goals 0 1 0)
      nil)))
+#


#+SYMBOLICS
(defun print-proof1 (goals goalnum ngoals level)
  (dotimes (i ngoals)
    (let ((arity (caar goals)) (goal (cadar goals)) (nsubgoals (caddar 
goals)) (number (cadddr (car goals))))
      (format t "~&(~3D)" goalnum)
      (cond ((consp number) (format t "~5D~A  " (car number) (cdr 
number)))
	    (number (format t "~5D   " number))
	    (t (princ "        ")))
      (dotimes (i level) (princ "   "))
      (write-functor-and-arguments (car goal) (subseq goal 1 (1+ 
arity)))
      (cond ((= nsubgoals 0) (princ ".") (setq goalnum (1+ goalnum)) 
(setq goals (cdr goals)))
	    (t (princ " <-")
	       (let ((first t))
		 (dolist (subgoal (collect-goals (cdr goals) nsubgoals))
		   (cond (first (princ " ") (setq first nil))
			 (t (princ " , ")))
		   (write-functor-and-arguments (car subgoal) (subseq subgoal 1 (1+ 
(get (car subgoal) 'arity))))))
	       (princ ".")
	       (multiple-value-setq (goals goalnum) (print-proof1 (cdr goals) 
(1+ goalnum) nsubgoals (1+ level)))))))
  (values goals goalnum))

#+SYMBOLICS
(defun collect-goals (goals ngoals)
  (let (w)
    (dotimes (i ngoals)
      (push (cadar goals) w)
      (setq goals (skip-goals (cdr goals) (caddar goals))))
    (nreverse w)))

#+SYMBOLICS
(defun skip-goals (goals ngoals)
  (dotimes (i ngoals)
    (setq goals (skip-goals (cdr goals) (caddar goals))))
  goals)