AI 中文总结
研究极小良定逻辑，提出未假定肯定前件规则的演算，构建由下半格类构成的语义，证明可靠性和完全性定理，还证明其重言式集可在多项式时间内判定并给出算法。
AI 中文摘要
研究了具有合取和蕴含的语言中的极小良定逻辑。提出了一种针对该逻辑的演算，其中未假定肯定前件规则。主要成果是为该逻辑构建了一种语义：它由具有最大元素的下半格类构成，其中蕴含通过基于半格偏序定义的部分函数来解释。证明了可靠性和完全性定理。所提出的语义为研究此类系统的有限模型性质问题创造了机会，也可作为研究极小良定逻辑本身及其扩展的其他性质的基础。作为所得结果的应用，证明了极小良定逻辑的重言式集在多项式时间内可判定，并给出了相应的判定算法。
英文摘要
The minimal well-determined logic in the language with conjunction and implication is investigated. A calculus for this logic, in which the modus ponens rule is not postulated, is proposed. The main result consists in constructing a semantics for this logic: it is formed by the class of lower semilattices with a greatest element, where the implication is interpreted using a partial function defined via the partial order of the semilattice. This extension of the notion of interpreting logical connectives in a matrix allows for the correct determination of the truth of formulas in the language with conjunction and implication. Soundness and completeness theorems are proved. The proposed semantics creates an opportunity to investigate questions of finite model property for such systems and can also serve as a basis for studying other properties of both the minimal well-determined logic itself and its extensions. As an application of the obtained results, we prove that the set of tautologies of the minimal well-determined logic is decidable in polynomial time and present a corresponding decision algorithm.
