Orador: Cristina Sernadas (Instituto Superior Técnico, CMAFcIO, 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.
Room 6.2.33 [⤴]