如何使计算机能运用常识进行推理和问题求解是人工智能领域最困难的问题之一,非单调逻辑是以此为目标的知识表示语言中最重要的一类。本论文致力于几种一阶非单调逻辑的可判定性和可译性研究。所获得的主要结果如下：第一,比较全面地研究了一阶限定理论及稳定语义下的一阶语言中各种前缀-符号集类在模型存在性意义下的可判定性。其中前缀-符号集类是通过对量词前缀、谓词、函词及等词作限制而定义的一种分类方式。具体地,本文找到了一阶限定理论中六个可判定的极大前缀-符号集类,找到了在稳定语义下可判定的一个极大前缀-符号集类,并找出了一大批不可判定类,从而得到了这两种语言在前述分类下关于可判定性与不可判定性比较精确的一个分界线。第二,系统研究了一阶限定理论、稳定语义下的一阶语言和各种析取逻辑程序之间的可译性关系。其中,根据翻译中是否允许辅助谓词和函词,以及问题的论域是有穷或不作限制,可译性关系被细分为四种。本文证明了上述语言在这四种关系下的绝大多数可译性或不可译性结果。这些结果对于理解存在量词、辅助谓词和函词、否定词的性质具有重要意义。特别地,由这些结果可以得到关于编码自然性方面的一些有趣结论,譬如可以推断存在一大类由逻辑程序可以表达的问题却不能使用一般论域中的编码技术在逻辑程序中进行编码。第三,研究了上述几种语言的模型论性质。特别地,证明了析取逻辑程序在稳定语义下满足下降Lowenheim-Skolem性质,即析取逻辑程序有稳定模型当且仅当它有可数稳定模型；证明了一阶稳定语义可刻画实数系统。因此,除非引入存在量词或其他机制,否则析取逻辑程序不能描述实数论域上的知识。第四,在可译性研究的基础上,对从稳定语义下一阶语言到逻辑程序的翻译进行了优化,设计并实现了稳定语义下一阶理论的一个原型求解器；通过在两个基准问题上的若干实验,验证了这一原型求解器的效率。此外,本文也给出了从一阶限定理论到稳定语义下一阶语言的一个非常简单的翻译,这将为设计高效的一阶限定理论求解器提供一条可行的技术途径。