Polyhedral Approaches to Selected Problems in Computational Logic

计算逻辑中选定问题的多面体方法

• 批准号: 0827397
• 负责人: Krishnamurthy Subramani
• 金额: $ 30.03万
• 依托单位: West Virginia University Research Corporation
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2009
• 资助国家: 美国
• 起止时间: 2009-02-15 至 2013-08-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=0827397&HistoricalAwards=false
• 关键词: Polyhedral; Approaches; Selected; Problems; Computational

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.

这个项目通过量化多面体编程的范例探索计算逻辑和多面体组合学之间的联系。量化多面体规划包括量化线性规划（QLP）和量化线性规划（QIP）;这两种编程范式在建模实时调度问题中的环境依赖行为时非常有用。量化的可验证程序还可以通过抽象解释机制来形式化地验证程序的正确性。这个项目的目的是提供一个框架，在这个框架中，传统的对偶和凸性概念可以扩展到2人游戏设置。例如，一个典型的优化问题是由一个优化函数和一个凸集定义的，称为可行域。在现实世界的应用中，如机器人导航，域是不固定的，但不断变化的结果，由环境发起的事件。因此，最优性的概念需要在2人设置中定义。在更广泛的方面，研究者计划通过创新研究和研究主题融入研究生和本科教育的结合，显着推进量化多面体编程的最新技术。 这项工作将增加妇女和代表性不足的少数民族在计算机科学研究的参与的额外好处。