论文部分内容阅读
在微机上用ＰＡＳＣＡＬ语言实现的命题演绎机器证明系统为背景，说明实现该证明系统的主要技术和技巧。证明了系统的算法和总体设计、公理模式和归约法则的建立、符号的处理、存储结构的选取、联结词消除以及输入输出处理等。对用微机来实现命题（谓词）证明系统提供了具有参考价值的意见。
微机证明系统的设计与实现
【摘 要】
：
在微机上用ＰＡＳＣＡＬ语言实现的命题演绎机器证明系统为背景，说明实现该证明系统的主要技术和技巧。证明了系统的算法和总体设计、公理模式和归约法则的建立、符号的处理、存储结构的选取、联结词消除以及输入输出处理等。对用微机来实现命题（谓词）证明系统提供了具有参考价值的意见。
【出 处】
：
重庆邮电学院学报
【发表日期】
：
1999年04期
其他文献
本文提出智能网络结点－－智能工作站的重要组成部分，即知识库系统中关系数据库与知识库的接口功能实现的数学模型。该模型是在分析关系数据库的关系模型和基于逻辑模式的知识库模型的基础上提出的，并研究了在该模型的基础上的推理查询方法。该数学模型对数据库智能化及将关系数据库扩展成知识库提供了有效的研究途径。
期刊
本文讨论了树图的集散函数和集散中心的性质。首先给出了树图集散函数的上、下确界以及给定集散函数值、树的存在性；然后讨论了集散的构成和树去掉一悬挂点后所得到的集散中心与原树集散中心的关系。
期刊
作者在本文中用差分格式对灰色ＧＭ（１，１）建模方法作了改进，建立了ＧＭ（１，１，λ）模型。文中给出了以误差平方和最小、误差绝对值之和最小、绝对百分误差和最小为目标的优化模型，同时还给出了三者为目标的多目标优化模型，求解λ值，进而对原始序列进行预测。由λ的取值知ＧＭ（１，１，λ）模型的精度一定比普通ＧＭ（１，１）模型高。实例分析效果是显著的，拟合精度非常高。
期刊
大学生素质的改善与提高，大量的是要通过教育来落实，诸如政治、思想、专业、心理健康等教育必须归结在学校，而辅导员是主要的实施者之一。辅导员的思想政治工作主要应是教育工作，其功能为：保证方向功能、感召垂范功能、协助教学活动顺利开展的功能、心理咨询功能、桥梁中介功能、沟通协调功能、是非评判功能和动员组织功能。
期刊
以进气道电磁散射的复射线分析为基础，研究了任意涂层进气道散射的２种常用方法，即射线追踪法和等效传输线法，结果表明，等效传输线法具有更好的实际工程应用价值。
期刊
针对目前实践性很强的技术基础课的实验课附属于理论课内，造成学生重理论、轻实验的思想状况，以《模拟电子技术》实验考核为例，从实验考核电路选择、实验考核方法、实验考核效果等方面进行了一些尝试，一定程度上改善了学生思想上重视实验的状况。
期刊