2017年7月1日—7日,逻辑自动推理领域的国际知名专家,德国DHBW Stuttgart大学计算机学院的Stephan Schulz教授应邀来到西南交通大学系统可信性自动验证国家地方联合工程实验室进行讲学。Stephan Schulz教授在自动推理理论、方法及其程序实现等方面做出了非常有影响的工作,其研发的自动定理证明器E是目前国际上最著名的证明器之一。
整个讲学过程一共组织了4次学术报告和若干次小范围交流。Stephan Schulz教授主要介绍了以下两方面的内容:第一,自动定理证明领域的最新进展,包括应用与需求、逻辑演算、证明搜索、自动定理证明系统与下一步发展等方面的最新情况;第二,自动定理证明器E,包括E的功能体系结构、E的软件体系结构与E的数据类型。
同时,实验室相关成员也给Stephan Schulz教授介绍了实验室原创的自动推理核心理论、并演示了实验室开发的相关自动定理证明器。针对实验室原创的理论与自动定理证明器,Stephan Schulz教授给出了宝贵的意见与建议。
针对理论研究、程序设计、实用工具开发等方面所遇到的问题,实验室成员同Stephan Schulz教授展开了热烈的讨论,并给出了一些很好的建议。这为促进更进一步的学术与技术交流,达成密切的合作关系奠定了很好的基础。