Skip to main content

Deciding satisfiability of formulas in the guarded negation fragment


Suitable for

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


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