Polyhedral Approaches to Selected Problems in Computational Logic

这个项目通过量化多面体编程的范例探索计算逻辑和多面体组合之间的联系。量化多面体规划包括量化线性规划(QLP)和量化整数规划(QIP)，这两种编程范型在实时调度问题的环境相关行为建模中都非常有用。量化的整数程序也可以通过抽象解释机制来形式化地验证程序的正确性。这个项目旨在提供一个框架，在这个框架中，传统的对偶和凸性概念可以扩展到两人游戏设置。例如，一个典型的优化问题由一个优化函数和一个称为可行域的凸集来定义。在现实世界的应用中，例如机器人导航，域不是固定的，而是随着环境启动的事件而连续变化的结果。因此，最优性的概念需要在两人的设置中定义。在更广泛的战线上，研究人员计划通过创新研究和将研究主题整合到研究生和本科教育中来显著推进量化多面体编程的最新水平。这项工作将有额外的好处，增加妇女和代表不足的少数民族参与计算机科学研究。该奖项由西弗吉尼亚州EPSCoR共同资助。

This project explores connections between computational logic and polyhedral combinatorics through the paradigm of Quantified Polyhedral programming. Quantified Polyhedral programming encompasses Quantified Linear Programming (QLP) and Quantified Integer Programming (QIP); both the programming paradigms are extremely useful in modeling environment-dependent actions in real-time scheduling problems. Quantified Integer Programs can also be used to formally verify the correctness of programs through the mechanism of Abstract Interpretation. This project aims to provide a framework in which traditional notions of duality and convexity can be extended to the 2-person game setting. For instance, a typical optimization problem is defined by an optimization function and a convex set, called the domain of feasibility. In real-world applications, such as robot navigation, the domain is not fixed but varies continuously as a consequence of events initiated by the environment. Thus, the concept of optimality needs to be defined in a 2-person setting.On a broader front, the investigator plans to significantly advance the state-of-the-art in Quantified Polyhedral Programming through a combination of innovative research and the integration of research themes into graduate and undergraduate education. This work will have the added benefit of increasing the participation of women and under-represented minorities in computer science research.This award is co-funded by West Virginia EPSCoR.