Este documento establece una conexión entre la teoría de control para sistemas de eventos discretos parcialmente observados (DESs) y la demostración automatizada de teoremas (ATP) en el cálculo de fórmulas positivamente construidas (PCFs). El lenguaje de PCFs es un lenguaje de primer orden completo que proporciona una herramienta potente para el análisis cualitativo de sistemas dinámicos. Basado en ATP en el cálculo de PCF, se sugiere una nueva técnica para verificar la observabilidad como una propiedad de lenguajes formales, que es necesaria para la existencia de control supervisado de DESs. En caso de violación de la observabilidad, las palabras que causan un conflicto también pueden ser extraídas con la ayuda de un PCF especialmente diseñado. Con un ejemplo del problema de planificación de ruta por un robot en un entorno desconocido, mostramos la aplicación de nuestro enfoque en uno de los niveles de un sistema de control de robot. También se presenta el probador Bootfrost desarrollado para facilitar la refutación de PCF. Las pruebas muestran resultados positivos y perspectivas para el enfoque presentado.