| 摘要 | 第1-4页 |
| ABSTRACT | 第4-6页 |
| 目录 | 第6-9页 |
| 1 绪论 | 第9-14页 |
| ·排队论起源 | 第9-10页 |
| ·数学问题计算机证明的发展现状及微分方面的发展近况 | 第10-12页 |
| ·用计算机自动证明排队论的意义 | 第12页 |
| ·本文主要研究的内容 | 第12-14页 |
| 2 排队论与计算机语言 | 第14-25页 |
| ·排队论预备知识 | 第14-19页 |
| ·排队系统描述 | 第14-16页 |
| ·排队系统记号 | 第16-17页 |
| ·排队系统指标 | 第17页 |
| ·排队论中有关概念 | 第17-19页 |
| ·MIZAR语言 | 第19-25页 |
| ·MIZAR文章结构 | 第19-21页 |
| ·MIZAR语言的数据类型和关键字 | 第21-22页 |
| ·MIZAR语言系统的定理证明的基本方法 | 第22-23页 |
| ·MIZAR语言的逻辑推理检验与优化 | 第23-25页 |
| 3 服务率可变的M/M/S/K模型研究 | 第25-37页 |
| ·M/M/S/K模型介绍 | 第25页 |
| ·模型假设 | 第25-26页 |
| ·状态转移图 | 第26-27页 |
| ·平稳分布 | 第27-30页 |
| ·主要指标 | 第30-33页 |
| ·统损失的概率 | 第30页 |
| ·平均损失顾客数 | 第30页 |
| ·进入系统的顾客数 | 第30-31页 |
| ·平均队长 | 第31-32页 |
| ·等待时间与逗留时间 | 第32-33页 |
| ·本章小结 | 第33-37页 |
| ·模型比较 | 第33-34页 |
| ·实例验证 | 第34-37页 |
| 4 一种服务率可变的串联排队服务系统研究 | 第37-47页 |
| ·模型假设 | 第37-38页 |
| ·马尔可夫过程 | 第38页 |
| ·服务台之间无排队位置的服务系统 | 第38-42页 |
| ·系统状态转移分析 | 第38-40页 |
| ·系统平衡方程 | 第40页 |
| ·系统指标分析 | 第40-42页 |
| ·服务台之间有排队位置的服务系统 | 第42-46页 |
| ·系统状态转移分析 | 第42-44页 |
| ·系统平衡方程 | 第44-45页 |
| ·系统指标分析 | 第45-46页 |
| ·本章小结 | 第46-47页 |
| 5 输入率与服务率依赖状态的M/M/C排队模型研究 | 第47-55页 |
| ·模型假设以及符号说明 | 第47-48页 |
| ·数学模型 | 第48-49页 |
| ·平稳分布 | 第49-52页 |
| ·主要指标 | 第52-53页 |
| ·顾客的平均输入率 | 第52页 |
| ·系统的平均服务强度 | 第52页 |
| ·平均队长 | 第52页 |
| ·服务机构繁忙率 | 第52-53页 |
| ·系统的损失概率 | 第53页 |
| ·本章小结 | 第53-55页 |
| 6 维修时间可变的有备用品的M/M/C/M+K/M模型研究 | 第55-63页 |
| ·问题叙述及假设 | 第55-56页 |
| ·维修工人数小于备用品的情形 | 第56-59页 |
| ·故障的机器数 | 第56-58页 |
| ·重要的指标 | 第58-59页 |
| ·维修工人数大于备用品的情形 | 第59-61页 |
| ·故障的机器数 | 第59-60页 |
| ·重要的指标 | 第60-61页 |
| ·本章小结 | 第61-63页 |
| 7 排队论中涉及微分的命题及其计算机实现 | 第63-76页 |
| ·微分几何中有关问题的介绍 | 第63-68页 |
| ·积分形式的转化原理 | 第63-64页 |
| ·多变量积分中的积分微元代换公式 | 第64-65页 |
| ·四个重要积分公式的同意描述 | 第65-68页 |
| ·Mizar数据库MML中关于微分几何方面的研究 | 第68页 |
| ·更新过程 | 第68-69页 |
| ·排队论基础问题的MIZAR实现 | 第69-75页 |
| ·环境部设置 | 第69-70页 |
| ·排队论中微分差分问题的MIZAR实现 | 第70-75页 |
| ·最终实现的MIZAR形式 | 第75-76页 |
| 总结与展望 | 第76-77页 |
| 参考文献 | 第77-80页 |
| 致谢 | 第80-81页 |
| 攻读学位期间发表的学术论文目录 | 第81-82页 |
