Para abordar los problemas de colisión semántica e inconsistencias entre ontologías y el modelo de datos original al aprender ontologías de bases de datos relacionales (RDB), se presenta un método de verificación de consistencia semántica semiautomático basado en representación gráfica intermedia y verificación de modelos. Inicialmente, se utilizó el W-Graph, como un modelo intermedio entre bases de datos y ontologías, para formalizar las correspondencias semánticas entre bases de datos y ontologías, que luego se transformaron en la estructura de Kripke y finalmente se codificaron con el programa SMV. Mientras tanto, se emplearon lógicas de descripción (DLs) para formalizar las especificaciones semánticas de las ontologías aprendidas, ya que el OWL DL mostró buena compatibilidad semántica y las DLs presentaron una excelente expresividad. Posteriormente, las especificaciones se convirtieron en una fórmula de lógica de árbol computacional (CTL) para mejorar la legibilidad por parte de la máquina. Además, la tarea de verificar la consistencia semántica podría convertirse en un problema de verificación de modelo global que podría resolverse automáticamente mediante el verificador de modelos simbólicos. Además, se proporciona un ejemplo para demostrar el proceso específico de formalización y verificación de la consistencia semántica entre ontologías aprendidas y RDB, y se llevó a cabo un experimento de verificación para comprobar la viabilidad del método presentado. Los resultados mostraron que el método presentado podía verificar e identificar correctamente los diferentes tipos de inconsistencias entre las ontologías aprendidas y su modelo de datos original.