In this thesis we explore a number of ways in which combinatorial games can be used to help prove results in the area of propositional proof complexity. The results in this thesis can be divided into two sets, the first being dedicated to the study of Resolution space (memory) requirements, whereas the second is centered on formalizing the notion of `dangerous' reductions. The first group of results investigate Resolution space measures by asking questions of the form, `Given a formula F and integer k, does F have a [Type of Resolution] proof with [Type of Resource] at most k?'. We refer to this as a proof complexity resource problem, and provide comprehensive results for several forms of Resolution as well as various resources. These results include the PSPACE-Completeness of Tree Resolution clause space (and the Prover/Delayer game), the PSPACE-Completeness of Input Resolution derivation total space, and the PSPACE-Hardness of Resolution variable space. This research has theoretical as well as practical motivations: Proof complexity research has focused on the size of proofs, and Resolution space requirements are an interesting new theoretical area of study. In more practical terms, the Resolution proof system forms the underpinnings of all modern SAT-solving algorithms, including clause learning. In practice, the limiting factor on these algorithms is memory space, so there is a strong motivation for better understanding it as a resource. With the second group of results in this thesis we investigate and formalize what it means for a reduction to be `dangerous'. The area of SAT-solving necessarily employs reductions in order to translate from other domains to SAT, where the power of highly-optimized algorithms can be brought to bear. Researchers have empirically observed that it is unfortunately possible for reductions to map easy instances from the input domain to hard SAT instances. We develop a non-Hamiltonicity proof system and combine it with additional results concerning the Prover/Delayer game from the first part of this thesis as well as proof complexity results for intuitionistic logic in order to provide the first formal examples of harmful and beneficial reductions, ultimately leading to the development of a framework for studying and comparing translations from one language to another.

In this thesis we explore a number of ways in which combinatorial games can be used to help prove results in the area of propositional proof complexity. The results in this thesis can be divided into two sets, the first being dedicated to the study of Resolution space (memory) requirements, whereas the second is centered on formalizing the notion of `dangerous' reductions. The first group of results investigate Resolution space measures by asking questions of the form, `Given a formula F and integer k, does F have a [Type of Resolution] proof with [Type of Resource] at most k?'. We refer to this as a proof complexity resource problem, and provide comprehensive results for several forms of Resolution as well as various resources. These results include the PSPACE-Completeness of Tree Resolution clause space (and the Prover/Delayer game), the PSPACE-Completeness of Input Resolution derivation total space, and the PSPACE-Hardness of Resolution variable space. This research has theoretical as well as practical motivations: Proof complexity research has focused on the size of proofs, and Resolution space requirements are an interesting new theoretical area of study. In more practical terms, the Resolution proof system forms the underpinnings of all modern SAT-solving algorithms, including clause learning. In practice, the limiting factor on these algorithms is memory space, so there is a strong motivation for better understanding it as a resource. With the second group of results in this thesis we investigate and formalize what it means for a reduction to be `dangerous'. The area of SAT-solving necessarily employs reductions in order to translate from other domains to SAT, where the power of highly-optimized algorithms can be brought to bear. Researchers have empirically observed that it is unfortunately possible for reductions to map easy instances from the input domain to hard SAT instances. We develop a non-Hamiltonicity proof system and combine it with additional results concerning the Prover/Delayer game from the first part of this thesis as well as proof complexity results for intuitionistic logic in order to provide the first formal examples of harmful and beneficial reductions, ultimately leading to the development of a framework for studying and comparing translations from one language to another.

Simplifier notre interaction avec les entités informatiques interconnectées de notre environnement et faciliter l'exploitation des informations générées par celles-ci est l'objectif des environnements et applications ubiquitaires. Le comportement des applications ubiquitaires dépend de l'état et de la disponibilité des entités (logicielles ou dispositifs) qui compose l'environnement ubiquitaire dans lequel ils évoluent, ainsi que des préférences et localisation des utilisateurs. Développer et exécuter des applications ubiquitaires est un véritable défi que notre approche essaie de relever au travers de l'environnement d'exécution ApAM. Considérant que l'environnement d'exécution est imprévisible, nous partons du principe qu'une application ubiquitaire doit disposer d'une grande flexibilité dans le choix de ses composants et que cette composition doit être automatique. Nous proposons une description abstraite et implicite de la composition (où les composants et les liens entre eux ne sont pas décrits explicitement), ce qui permet de construire l'application incrémentalement pendant la phase d'exécution. La plate-forme d'exécution ApAM implémente ces mécanismes de composition incrémentale et s'en sert pour conférer aux applications ubiquitaires la capacité de « résister » et de s'adapter aux changements imprévisibles de l'environnement d'exécution. Cette propriété dite de résilience est au cœur de notre approche car elle permet aux programmeurs de développer « simplement » des applications « résilientes » sans avoir à décrire les diverses adaptations à réaliser, et même sans connaitre toutes les perturbations de l'environnement auquel elles seront soumises. Notre proposition offre le moyen de développer et d'exécuter des applications ayant un haut niveau de résilience vis-à-vis des évolutions de leur contexte d'exécution, grâce à des mécanismes automatiques capables de construire et de modifier à l'exécution l'architecture logicielle des applications ubiquitaire. Les mécanismes fournis sont génériques mais peuvent être étendus et spécialisés pour s'adapter plus finement à certaines applications ou à des domaines métiers spécifiques. / The goal of ubiquitous environments and applications is to simplify our interaction with interconnected software and hardware entities, and to allow the exploitation of the information that they gather and generate. The behavior of ubiquitous applications depends on the state and the availability of the software and hardware entities that compose the ubiquitous environment in which they are constantly evolving, as well as, the preferences and locations of users. Developing and executing ubiquitous applications is a difficult challenge that our approach attempts to address with the creation of the ApAM execution environment. Knowing that the execution environment is unpredictable, we believe that ubiquitous applications require a large amount of flexibility in choosing the components that compose the application, and that the composition should be automated. We propose an abstract and implicit description of the composition, where components and bindings are not explicitly described. This allows to incrementally building an application at runtime. The ApAM execution platform implements the mechanisms to achieve incremental composition and uses them to provide ubiquitous applications with the resilience and adaptability necessary to face unpredictable changes that originate in the execution environment. Resilience is a core property of our approach because it allows developers to easily build applications without the need to either describe nor predict the multiple adaptations required to support environmental disturbances which the applications will encounter. Our proposal offers the means of developing and executing applications with a high level of resilience in regards to their continuously evolving context. This is possible thanks to the mechanisms described in this dissertation that allow building and changing, at runtime, ubiquitous applications. These mechanisms are generic but can be extended or specialized in order to solve domain or application-specific issues.