Skip to main content

Extensible Search-Based Theorem Prover


Mark Kaminski

Suitable for

MSc in Computer Science
Mathematics and Computer Science, Part C
Computer Science, Part C
Computer Science and Philosophy, Part C


"Background: Search-based proof methods such as those based on DPLL, tableau and connection calculi are widely used in automated theorem proving, ontological reasoning, and automated verification. As most implementations of such methods are developed with a particular logic, algorithm, and set of applications in mind, it is often difficult to extend them with new features.

Project goals: The project aims to develop a modular, extensible base for implementing search-based decision procedures for propositional, modal, and description logics. A key objective is to develop an abstract proof search engine that can be instantiated with different logics, proof rules, and search strategies. The capabilities of the engine should be demonstrated by implementing a simple tableau-based or DPLL-based reasoner for propositional or modal logic. Prerequisites: good functional programming skills, familiarity with logic and automated theorem proving.