Reconstructing a single-head formula to facilitate logical forgetting
Artificial Intelligence
2020-12-21 v1 Logic in Computer Science
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.
Keywords
Cite
@article{arxiv.2012.10191,
title = {Reconstructing a single-head formula to facilitate logical forgetting},
author = {Paolo Liberatore},
journal= {arXiv preprint arXiv:2012.10191},
year = {2020}
}