• 主题
高级搜索  >
历史搜索 清空历史
首页> 美国政府科技报告 >Combining Automated Theorem Provers with Symbolic Algebraic Systems: Position Paper
【24h】

Combining Automated Theorem Provers with Symbolic Algebraic Systems: Position Paper

机译：将自动定理证明与符号代数系统相结合：立场文件

获取原文
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

In contrast to pure mathematical applications where automated theorem provers (ATPs) are quite capable, proof tasks arising form real-world applications from the area of Software Engineering show quite different characteristics: they usually do not only contain much arithmetic (albeit often quite simple one), but they also often contain reasoning about specific structures (e.g. graphics, sets). Thus, an ATP must be capable of performing reasoning together with a fair amount of simplification, calculation and solving. Therefore, powerful simplifiers and other (symbolic and semi-symbolic) algorithms seem to be ideally suited to augment ATPs. In the following we shortly describe two major points of interest in combining SASs (symbolic algebraic systems) with top-down automated theorem provers (here: SETHEO (Let92, GLMS94)).

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱：kefu@zhangqiaokeyan.com

京公网安备：11010802029741号 ICP备案号：京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有

  • 客服微信

  • 服务号