Article ID | Journal | Published Year | Pages | File Type |
---|---|---|---|---|
428814 | Information Processing Letters | 2016 | 4 Pages |
Abstract
•Prenex normal forms (PNF) of logical sentences are often used computational logic.•Converting to PNF with the standard method can lead to exponentially larger formulas.•We show that the conversion is possible with polynomial growth.
The textbook method for converting a first-order logic formula to prenex normal form potentially leads to an exponential growth of the formula size, if the formula is allowed to use all of the classical logical connectives ∧, ∨, →, ↔, ¬. This note presents a short proof which shows that the conversion is possible with polynomial growth of the formula size.
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics
Authors
Frederik Harwath,