Reconstructing a single-head formula to facilitate logical forgetting

2020/12/18 by Paolo Liberatore, Liberatore, Paolo
Computer Science · #Artificial Intelligence (cs.AI) #FOS: Computer and information sciences #Intelligent Tutoring Systems and Adaptive Learning #Logic in Computer Science (cs.LO) #Machine Learning and Algorithms #Topic Modeling

paper · pdf · doi:10.48550/arxiv.2012.10191

openalex publication_date 2020/12/18 · openalex created_date 2025/10/10 · openalex updated_date 2026/08/04

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.

Related

• One head is better than two: a polynomial restriction for propositional definite Horn forgetting
• Four algorithms for propositional forgetting
• Common equivalence and size after forgetting
• The ghosts of forgotten things: A study on size after forgetting
• Abductive forgetting