基于抽象解释的逻辑程序验证研究

利用逻辑程序设计语言开发正确、可靠且具有较高效率的软件系统是逻辑程序设计领域研究的热点。本项目主要研究基于抽象解释逻辑程序验证方法的完备性问题以及ASP(Answer Set Programming)在基于抽象解释逻辑程序验证中的应用。项目整合抽象解释、抽象调试和抽象域精化技术为逻辑程序验证中完备性问题的解决提供了一条新途径；ASP的应用则提供了一种传统基于抽象解释逻辑程序验证方法之外的新技术。本项目将构建逻辑程序完备验证和基于反例导向抽象域精化的逻辑程序验证算法框架，设计并实现利用ASP验证逻辑程序的高效算法，该研究具有学术创新性。开发采用以上技术的逻辑程序验证系统，将为人工智能系统软件的开发提供有效的技术支持。