在APPLEII机上实现自动定理证明

来源 :微计算机应用 | 被引量 : 0次 | 上传用户：tp20201892

【摘要】

：

<正> 作者根据锁归结(lock resolution)原理用LISP语言编制了完整的框图和程序,并在APPLE Ⅱ机器上实现了对命题逻辑中的定理的证明。归结原理的证明过程采用了反驳(refutati

【作者】

：

吴茂康

【机构】

：

上海科技大学

【出处】

：

微计算机应用

【发表日期】

：

1990年2期

【关键词】

：

微机自动定理证明命题逻辑

下载到本地 , 更方便阅读

下载此文赞助VIP

声明 : 本文档内容版权归属内容提供方 , 如果您对本文有版权争议 , 可与客服联系进行内容授权或下架

论文部分内容阅读

<正> 作者根据锁归结(lock resolution)原理用LISP语言编制了完整的框图和程序,并在APPLE Ⅱ机器上实现了对命题逻辑中的定理的证明。归结原理的证明过程采用了反驳(refutation)的形式,这很像数学中的反证法。为了使一个定理能在计算机上得以证明,首先要把定理的前提和结论都化为逻辑表达式,然后把定

其他文献

园林建设工程施工组织设计编制实例：‘99昆明世博园澳大利亚展园施工组织设

通过对世博园国际室外展园的施工实践。总结园林绿化工程施工组织设计的编制步骤、要点、并探讨主要园林工程项目的施工方法。

期刊

世博园澳大利亚展园施工组织技术管理

雷州刚果12号桉（W5无性系）二元立木材积表的编制

在雷州林业局１０个林场中的廉江、石岭、遂溪、北坡、河头、纪家、龙门等７个林场，以三个不同的立地类型为划分依据，再结合不同的林分生长类型设典型样地２３个，共收以样木１６３６株，用ＥＸＣＥＬ２０００软件中的ＬｉｎｅｓｔＯ函

期刊

刚果12号桉无性系立木材积表适应性数学模型

美国远程教育规范中的社会文化因素

作为当今世界教育最为发达国家之一的美国,“民主”、“实用”、“科学”既是其教育追求的目标,也是其教育的总特点。美国远程教育体系性的重要体现,就是形成了较为完善的法

期刊

美国远程教育规范社会文化American distance education norms social culture

轻钢结构厂房消防设计中一些问题的探讨

本文结合实际设计经验，探讨了轻钢结构工业厂房消防设计中的耐火等级、防火分区、防火墙、卷帘、水幕等问题。

期刊

轻钢结构工业厂房耐火等级防火分区消防设计

C语言与FORTRAN语言接口原理

用异种程序设计语言编写的程序模块,要实现相互调用,必须解决不同语言环境之间转换的接口。在一些配置了UNIX操作系统的小型、微型计算机上,仅提供了FORTRAN,PASCAL程序调用C

期刊

C语言FORTRAN语言接口程序设计

原发咽旁滑膜肉瘤1例

本文报告1例咽旁滑膜肉瘤,患者男,15岁,以左咽旁无痛性逐渐增生包块1月就诊。专科检查发现左侧咽旁有一大小约8 cm×4 cm×3 cm肿物,蒂部位于左扁桃体上隐窝。影像学

期刊

滑膜肉瘤咽旁治疗synovial sarcoma pharynx treatment

日本考察散记

期刊

日本林业林业教育城市林业森林旅游

我国教师教育的发展趋势与教育专业自学考试的改革对策

我国教师教育已经呈现出终身化、多元化、高层化、专业化、综合化、信息化等发展趋势,教育专业自学考试必须拓展考试功能,提升考试层次,调整专业设置和学科比例,变更培养目标

期刊

教师教育教育专业自学考试培养目标课程设置teacher education education disciplines self-study e

乳化降黏剂的制备及其在油田单管集油中的应用

针对大庆油田单管通球集输试验井采出液黏度高、集油阻力大，部分油井出油压力长期偏高导致井口漏油以及抽油杆滞后等问题，开发了能减小油井集油阻力和降低出油压力的原油乳化降

期刊

单管集油乳化降黏剂加药浓度压力single tube oil gatheringemulsifying viscosity reducerdosin

埃克森美孚第三季度利润超过62亿美元

埃克森美孚公司(Exxon Mobil Corporation)宣布,其2018年第三季度盈利预计为62亿美元,合每股1.46美元,上年同期利润为40亿美元。运营和资产出售的总现金流为126亿美元,其中资

期刊

利润埃克森美孚公司天然气开发资产出售EXXON首席执行官日产量物流网络

在APPLEII机上实现自动定理证明

与本文相关的学术论文