11 DEZEMBRO / SEGUNDA FEIRA / 13:16
FCUP PT 
 EN
 
 
APRESENTAÇÃO
PESSOAS
ENSINO
INVESTIGAÇÃO
BIBLIOTECA
NOTÍCIAS
CONTACTOS

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


FCUP 2017