Computational logic is the study of logic and logical methods within computer science. Logic is the study of valid inferences, and in computational logic it is studies how to automate such inferences on a computer. Computational logic is used for the specification and verification of software and hardware systems, for topics in databases and programming languages, and for logic-based AI, such as automated reasoning and knowledge-based systems.
The section’s research in this area includes: Modal logic, hybrid logic, temporal and interval logics for specification and verification, tableau-based logical decision procedures, higher-order logic, non-classical logic, array-based logic and systems, algorithms for proof systems, multi-agent systems, knowledge-based systems, formal ontologies, and argumentation theory using ontological semantics.