我有一个应该在cnf中转换wff的函数,该函数的一部分不想工作,我设法查明了问题,这是代码
(defun skole-gay (fbf &optional (var-for nil) (var-ex nil))
(if (consp fbf)
(case (car fbf)
(forall ;nel caso di forall salvo il prossimo elemento assieme a possibile altri elementi di altri forall
(skole-gay (third fbf) (cons (second fbf) var-for) var-ex))
(exist ;nel caso di exist salvo il suo elemento
(skole-gay (third fbf) var-for (cons (second fbf) var-ex)))
((car var-ex) ;nel caso che trovo l'elemento salvato della exist faccio dei contrllo per vedere cosa devo fare
(cond
((eql (car var-for) nil) ;se sub-for e' vuoto vuol dire che non ci sn stati forall indi devo solo inserire la const
(cons (skolem-variable)
(skole-gay (cdr fbf) nil var-ex))) ;dopo la costante metter il resto della fbf
((not(eql (car var-for) nil)) ;ci sono stati forall
(cons (skolem-function var-for)
(cons (car var-for) (skole-gay (cdr fbf) nil var-ex))))))
((and or) ;se trovo and or not semplicemente li riscrivo e continuo con la ricorsione
(list (car fbf) (skole-gay (second fbf) var-for var-ex) (skole-gay (third fbf) var-for var-ex)))
((not) ;se trovo and or not semplicemente li riscrivo e continuo con la ricorsione
(list (car fbf) (skole-gay (second fbf) var-for var-ex)))
(otherwise
;; e' solo 1 proposizione, la ritorno
fbf))
fbf))
有一次我在做 (case (car fbf) ; 其中 fbf = ?x 的汽车,其中一种情况是 ((car var-ex) ; 那时他们的程序也是 ?x 但它不运行那部分程序,我不知道为什么,
忽略代码中的注释,因为它们是意大利语