Technical Report: DCC-98-1
Short proofs for MIU theorems
Armando B. Matos, Luis Filipe Antunes
DCC & LIACC
Universidade do Porto
Rua do Campo Alegre, 823 4150 Porto, Portugal
February 1998
Abstract
We study the MIU formal system, characterizing all possible theorems.
We propose an algorithm to prove that a givem formula
t is a theorem,
and based on that algorithm we prove that the number of lines of a minimum
line proof is
O(max{n_u,log|t|}) and the number of symbols
of a minimum line proof is
O(max{n_u|t|,|t|}), where
n_u
is the number of u's in the proof.
Keywords: Complexity of proofs, Formal Systems
