Reconstructing a single-head formula to facilitate logical forgetting

TL;DR

This paper presents a complete algorithm for converting propositional definite Horn formulas into single-head form, enabling efficient logical forgetting by avoiding exponential complexity.

Contribution

It introduces a new, complete algorithm that always finds an equivalent single-head formula if one exists, improving upon previous incomplete methods.

Findings

The algorithm guarantees a single-head equivalent formula when possible.

It reduces the complexity of logical forgetting for single-head formulas.

The method outperforms previous approaches by ensuring completeness.

Abstract

Logical forgetting may take exponential time in general, but it does not when its input is a single-head propositional definite Horn formula. Single-head means that no variable is the head of multiple clauses. An algorithm to make a formula single-head if possible is shown. It improves over a previous one by being complete: it always finds a single-head formula equivalent to the given one if any.