Creating and sharing knowledge for telecommunications

on 21-07-2014

The poster «Display Scalable 3D Holoscopic Video Coding» by Caroline Conti, Luis Ducla Soares and Paulo Nunes has won the Best Poster competition of COST training school on Rich 3D Content: Creation, Perception and Interaction in Budapest, Hungary, on July 2014.

http://3d-contournet.eu/interaction2014/2014/07/21/the-best-poster-award/on 17-07-2014

Edward Hauesler, PUC - Rio de Janeiro, Brasil

July 17, 2014, Thursday, 16h15m.

Abstract: In 1979 Richard Statman proved, using proof-theory, that the purely implicational fragment of Intuitionistic Logic is PSPACE-complete. He showed a polynomially bounded translation from full Intuitionistic Propositional Logic into its implicational fragment. By the PSPACE-completeness of S4, proved by Ladner, and the Godel translation from S4 into Intuitionistic Logic, the PSPACE-completeness of purely implicational fragment of Intuitionistic Logic is drawn. The sub-formula principle for a deductive system for a logic L states that whenever {γ1,…,γk}⊢Lα there is a proof in which each formula occurrence is either a sub-formula of α or of some of γi. In this work we extend Statman's result and show that any propositional (possibly modal) structural logic satisfying a particular statement of the sub-formula principle is PSPACE-complete. As a consequence, EXPTIME-complete propositional logics, such as PDL and the common-knowledge epistemic logic with at least 2 agents satisfy this particular sub-formula principle, if and only if, PSPACE=EXPTIME.

In 1979 Richard Statman proved, using proof-theory, that the purely implicational fragment of Intuitionistic Logic is PSPACE-complete. He showed a polynomially bounded translation from full Intuitionistic Propositional Logic into its implicational fragment. By the PSPACE-completeness of S4, proved by Ladner, and the Godel translation from S4 into Intuitionistic Logic, the PSPACE-completeness of purely implicational fragment of Intuitionistic Logic is drawn. The sub-formula principle for a deductive system for a logic L states that whenever {γ1,…,γk}⊢Lα there is a proof in which each formula occurrence is either a sub-formula of α or of some of γi. In this work we extend Statman's result and show that any propositional (possibly modal) structural logic satisfying a particular statement of the sub-formula principle is PSPACE-complete. As a consequence, EXPTIME-complete propositional logics, such as PDL and the common-knowledge epistemic logic with at least 2 agents satisfy this particular sub-formula principle, if and only if, PSPACE=EXPTIME.

Room: 3.10, Mathematics

Support: SQIG/Instituto de Telecomunicações with support from FCT and FEDER namely by the FCT project PEst-OE/EEI/LA0008/2013.

© 2020, IT - Instituto de Telecomunicações | All Rights Reserved