Abstract
In this paper, we consider the free-variable variant of the calculus KE and investigate the effect of different preprocessing activities to the proof length of variants of KE. In this context, skolemization is identified to be harmful as compared to the δ-rule. This does not only have consequences for proof length in KE, but also for the “efficiency” of some structural translations. Additionally, we investigate the effect of quantifier-shifting and quantifier-distributing rules, respectively. In all these comparisons, we identify classes of formulae for which a non-elementary difference in proof length occur.
Cite
CITATION STYLE
Egly, U. (1999). Quantifiers and the System KE: Some surprising results. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1584, pp. 90–104). Springer Verlag. https://doi.org/10.1007/10703163_7
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
