La Lógica es un pilar fundamental en el desarrollo de las Matemáticas y la Informática, desde los aspectos orientados al hardware (diseño y verificación de circuitos) hasta el software (manejo de consultas de bases de datos, verificación formal de programas, etc.) y, sobre todo, en el campo de las Ciencias de la Computación y la Inteligencia Artificial.

El proyecto LogicUS, iniciado desde el Departamento de Ciencias de la Computación e Inteligencia Artificial de la Universidad de Sevilla, ofrece un sistema de apoyo a la enseñanza de la Lógica Computacional. Su objetivo es proporcionar las herramientas necesarias, en diferentes niveles de abstracción, para el tratamiento de la Lógica orientada a la resolución de problemas en diferentes aspectos de la Lógica Proposicional (LP/PL) y de Primer Orden (LPO/FOL). Estas herramientas, basadas en el uso de la programación funcional y con una orientación web, proporcionan un conjunto de algoritmos operativos que facilitan la asimilación de los conceptos fundamentales de la Lógica (tableros semánticos, DPLL, resolución, Herbrand, etc.).

El sistema LogicUS está diseñado para representar las ejecuciones y resultados de estos algoritmos en diferentes formatos (tablas, gráficos, ...) específicamente diseñados para permitir la integración con otros sistemas y herramientas. En concreto, facilita la generación de documentos exportables en diferentes formatos. De esta forma, proporcion un conjunto completo de herramientas para apoyar el desarrollo docente en Lógica Computacional de forma interactiva durante el desarrollo de las sesiones teóricas de docencia, generación de documentación de apoyo, creación de prácticas y pruebas de evaluación.

El sistema LogicUS está diseñado de forma modular, abierta, gratuita, ligera, e incluso colaborativa, para la enseñanza de la Lógica en el contexto de diferentes disciplinas científicas.