(defun fbf-fun (fbf)
(or (negazione fbf)
(cong fbf)
(disg fbf)
(implicazione fbf)
(universale fbf)
(existenciale fbf)
(predicato fbf)))
(defun negazione (fbf)
(and (eq (first fbf) 'not)
(fbf-fun (second fbf))
(= (length fbf) 2)))
(defun cong (fbf)
(and (eq (first fbf) 'and )
(reduce (lambda (x y) (and x y))
(mapcar #'fbf-fun (rest fbf)))))
(defun disg (fbf)
(and (eq (first fbf) 'or)
(reduce (lambda (x y) (and x y))
(mapcar #'fbf-fun (rest fbf)))))
(defun implicazione (fbf)
(and (eq (first fbf) '==>)
(fbf-fun (second fbf))
(fbf-fun (third fbf))
(= 3 (length fbf))))
(defun universale (fbf)
(and (eq (first fbf) 'forall)
(variabile (second fbf))
(fbf-fun (third fbf))
(= 3 (length fbf))))
(defun existenciale (fbf)
(and (eq (first fbf) 'exist)
(variabile (second fbf))
(fbf-fun (third fbf))
(= 3 (length fbf))))
(defun costante (fbf)
(or (numberp fbf)
(alpha-char-p (char (string 'fbf) 0))))
(defun variabile (fbf)
(and (symbolp fbf)
(char= #\? (char (symbol-name fbf) 0))))
(defun funzione (fbf)
(and (symbolp (first fbf))
(or (reduce (lambda (x y) (and x y))
(mapcar #'termine (rest fbf)))
(null (rest fbf)))))
(defun termine (fbf)
(or (costante fbf)
(variabile fbf)
(funzione fbf)))
(defun predicato (fbf)
(or (and (symbolp fbf)
(alpha-char-p (char (string 'fbf) 0)))
(and (symbolp (first fbf))
(or (reduce (lambda (x y) (and x y))
(mapcar #'termine (rest fbf)))
(null (rest fbf))))))