Logische Formeln dienen der Beschreibung und der Analyse von Systemen und komplexen Sachverhalten. Dabei reicht das Spektrum der verwendeten Logiken von der Aussagenlogik (z. B. bei Booleschen Netzen) bis hin zur Prädikatenlogik und deren Varianten und Fragmenten. Bereits das aussagenlogische Erfüllbarkeitsproblem (SAT) stellt eine algorithmische Herausforderung dar. Es geht zum einen um die komplexitätsmäßige Einordnung der fraglichen Logiken, zum anderen um die Konstruktion und Analyse entsprechender Algorithmen, Kalküle und Programmiersprachen zur Lösung logischer Fragestellungen. Derartige Ansätze enthalten vielfach neuartige probabilistische und heuristische Konzepte, die weiterentwickelt, theoretisch analysiert und/oder experimentell getestet werden müssen.