在日常生活中,人类经常利用常识进行推理。这种推理的前提或结论中包含常识判断,可以为人类的行动提供理由与指导。从语言角度而言,典型的常识判断包含常识蕴涵与概称句两类。由于这两类常识判断的完整形式分别与实质蕴涵和全称句不同,常识推理具有一些特殊的推理性质,并且这些性质不能被经典逻辑所刻画。为了能够刻画这些推理性质,周北海、毛翊与张立英等学者基于模态逻辑的方法,给出了一系列常识推理系统。在其中,M是极小系统,被称作“常识推理的基础逻辑”。该系统可以刻画与“常识蕴涵分离”有关的推理模式,具有良好的哲学直观,因此在常识推理逻辑的研究中极为重要。在形式语义学方面,周北海与毛翊建立了M的集选函数语义,并将其推广到其他常识推理逻辑中。通过“Γ-典范模型”方法,他们证明了 M在该语义下的完全性与有穷模型性,由此得到M的可判定性。虽然M可以刻画诸多常识推理特征,且具有直观的形式语义,其自身依旧具有很多技术上的缺陷。首先,集选函数语义的使用繁琐复杂,尤其是反模型构造以及完全性证明困难。其次,M目前只有公理化系统。但公理化系统并不具有好的证明论性质,在内定理与原定理的证明中缺乏构造性。这限制了该类逻辑的使用与推广。本文以常识推理逻辑的语义与证明论为研究对象,聚焦于M及其增加等同公式以及传递公式的扩张系统M1与M2,旨在解决以上所提到的问题与缺陷。首先,本文研究了 M的代数语义。该语义具有普遍性,可以简单迁移到M的扩张系统中。其同时也是一种强大的工具,能够利用代数的性质研究对应逻辑系统的性质。本文给出了 M对应的代数,并且通过林登鲍姆-塔斯基方法证明了 M的代数完全性。M1与M2的代数语义可以使用类似方法建立。其次,本文研究了 M的选择函数语义以及邻域语义。前者的优势在于具有良好的哲学直观,后者则易于构造反模型。基于切拉斯（B.Chellas）以及纳特（D.Nute）的工作,本文分别给出了一个M的选择函数模型以及邻域模型,并且证明了可靠性。通过林登鲍姆-塔斯基（Lindenbaum-Tarski）构造,本文给出了邻域模型相对于M具有典范性的充分必要条件。根据该条件,真引理对于任意典范模型成立。然而,并非任意的完全一致集的集合都存在特征公式与之对应,因此无法直接得到M在这两种语义下的完全性。最后,本文研究了 M的结构证明论。基于奥利维蒂（N.Olivetti）以及波扎托（G.L.Pozzato）的工作,本文给出了一个新的加标矢列系统LM,并且证明了 LM与M的等价性。通过类似方法,本文还给出了分别与M1和M2等价的加标矢列系统LM1与LM2。