Logical forgetting is removing some variables from a formula while maintaining its consequences on the remaining variables. This removal may require exponential time on arbitrary propositional Horn formulae, but it only takes polynomial time on single-head propositional definite Horn formulae. 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 enlarges the set of formulae admitting polynomial-time forgetting by making them single-head if possible and then running the usual algorithm for forgetting.
Reconstructing a single-head formula to facilitate logical forgetting / Liberatore, P.. - In: JOURNAL OF LOGIC AND COMPUTATION. - ISSN 0955-792X. - 33:7(2023), pp. 1596-1624. [10.1093/logcom/exac086]
Reconstructing a single-head formula to facilitate logical forgetting
Liberatore P.
2023
Abstract
Logical forgetting is removing some variables from a formula while maintaining its consequences on the remaining variables. This removal may require exponential time on arbitrary propositional Horn formulae, but it only takes polynomial time on single-head propositional definite Horn formulae. 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 enlarges the set of formulae admitting polynomial-time forgetting by making them single-head if possible and then running the usual algorithm for forgetting.File | Dimensione | Formato | |
---|---|---|---|
Liberatore_Reconstructing_2023.pdf
accesso aperto
Note: https://doi.org/10.1093/logcom/exac086
Tipologia:
Versione editoriale (versione pubblicata con il layout dell'editore)
Licenza:
Creative commons
Dimensione
595.51 kB
Formato
Adobe PDF
|
595.51 kB | Adobe PDF |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.