排队论在科学技术与国民经济的发展中起了重要的作用，也是通信，计算机等领域的专家学者必不可少的数学工具，当前排队服务系统的输入率与服务率依赖系统状态等相关问题受到学者的广泛关注，于是深入研究排队论中若干问题以及实现排队论复杂问题的计算机逻辑证明，成为当今研究的重要课题。　　Mizar语言系统是用于证明数学问题的一种语言系统，在数学命题的自动推理与证明的过程中逐步发展与完善。现在Mizar系统可智能化实现逻辑证明，复杂计算，校验排版等，并拥有世界上最大的数据库MML。　　本文首先对排队论以及Mizar语言系统进行了简单描述，然后对输入率和服务率依赖状态的排队模型进行了详细探讨，在此基础上，详细计算并给出了衡量排队论的重要指标，利用数学问题自动推理系统Mizar，以及微分几何知识，对排队论中的更新过程等问题进行了Mizar智能化推理，并且通过了系统验证。本文主要的工作如下:　　1、考虑输入率和服务率依赖系统状态，对M/M/s/K模型讨论了服务率可变的情形;对M/M/c模型同时考虑服务率和输入率可变的情形;对M/M/c/m+K/m模型考虑服务率可变的情形;对两个服务台串联模型考虑服务率可变的情形。对以上四个问题，本文都给出了严格的数学证明，并对每个模型进行深入研究，论证了系统的平稳分布，并得出系统中顾客的平均输入率，系统的平均服务强度，系统顾客的损失等衡量排队论性能的重要指标。　　2、首次用Mizar语言证明排队论问题，结合微分几何理论中微分差分等Grassmann代数理论，实现了排队论中几个问题的Mizar智能化推导证明。