Linear lower bounds and simulations in Frege systems with substitutions
Visualitza/Obre
Estadístiques de LA Referencia / Recolecta
Inclou dades d'ús des de 2022
Cita com:
hdl:2117/97081
Tipus de documentReport de recerca
Data publicació1996-10
Condicions d'accésAccés obert
Tots els drets reservats. Aquesta obra està protegida pels drets de propietat intel·lectual i
industrial corresponents. Sense perjudici de les exempcions legals existents, queda prohibida la seva
reproducció, distribució, comunicació pública o transformació sense l'autorització del titular dels drets
Abstract
Our work concerns Frege systems,
substitution Frege systems (sF),
renaming Frege systems, top/bottom-Frege systems and
extended Frege systems (eF).
Urquhart shows that tautologies associated to a binary
strings require Omega(n/log n) lines
to be proved in sF.
Here we prove, by giving a sF proof
of O(n/log n) lines in substitution Frege, that his
lower bound is optimal and we show that
in the tree-like case
Omega(n) lines are required for a proof
of the same tautologies.
We also show the following two simulation results:
(1) tree-like substitution Frege p-simulates non
tree-like substitution Frege; (2) Tree-like Frege
linearly simulates tree-like renaming Frege
and tree-like top/bottom-Frege.
CitacióBonet, M., Galesi, N. "Linear lower bounds and simulations in Frege systems with substitutions". 1996.
Forma partLSI-96-60-R
Fitxers | Descripció | Mida | Format | Visualitza |
---|---|---|---|---|
1400265416.pdf | 1,619Mb | Visualitza/Obre |