Por Cristina Sernadas (Instituto Superior Técnico, CMAF-CIO, Universidade de Lisboa).
Abstract: Relying on the notion of FOL schema calculus, we define the descriptive complexity of a schema formula given a set of schema formulas as the number of symbols of the smallest schema derivation of the schema formula from the set. We prove uniform schema robustness results in a schema calculus guided by the constructors of schema FOL, that is, we relate the descriptive complexity of introducing a logical constructor in terms of the descriptive complexity of the component schema formulas. Moreover, we also relate the descriptive complexities of a schema formula across different schema calculi related by a translation schema. Given a FOL signature, the descriptive complexity of a formula given a set of formulas is defined in terms of the descriptive complexity of the corresponding schema formulas. Finally, we show that from any concrete derivation over a signature it is always possible to extract an appropriate schema derivation. We illustrate the concepts and results using Hilbert and Gentzen formulations.
Joint work with João Rasga and Jaime Ramos.
