Proof Theoretical Implementations of Computer Science Logic

Proving that some statement follows from a collection of other statements using the rules of a given (hybrid nonclassical) logic plays a fundamental role in Computer Science areas like Hardware Verification, Database Security, and Intelligent Agents. Current proof search implementations either target a specific logic, or a small collection of related logics. We will implement a single, extremely general, (hybrid nonclassical) framework, called Display Logic, at two levels of specialisation: the first for interactive human-guided proof search; and the second for rapid development and testing of prototypes for automatic proof-search.