###
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