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