Supervisor

Suitable for

Abstract

The guarded negation fragment of first-order logic is an expressive logic of interest in databases and knowledge representation. It has been shown to have a decidable satisfiability problem but, to the best of my knowledge, there is no tool actually implementing a decision procedure for it.

The goal would be to design a tool to determine whether or not a formula in this logic is satisfiable. Most likely, this would require designing and implementing a tableau-based algorithm, in the spirit of related tools for description logics and the guarded fragment.

Prerequisites: Logic and Proof (or equivalent). There are some connections to material in Knowledge Representation and Reasoning, but this is not essential background