| 摘要: |
| 标记逻辑是一种重要的次协调逻辑，和｜≈是标记逻辑中的２种推理关系．二者都是次协调的，可以用统一的方法处理一致的知识与不一致的知识，是单调的，有基于归结的证明论，但不能保持经典逻辑中合理的推理，如三段论．｜≈是非单调的，在前提一致时等价于经典逻辑的推理关系，但缺少有效的证明论．本文将给出推理关系和｜≈基于Ｔａｂｌｅａｕ演算的可靠而且完备的判定方法. |
| 关键词: 标记逻辑 Tableau方法 择优蕴涵 次协调逻辑 |
| DOI： |
| 分类号: |
| 基金项目:本文研究得到国家自然科学基金和国家863高科技项目基金资助. |
|
| TABLEAU CALCULUS FOR ANNOTATED LOGIC |
|
Cheng Xiaochun,Liu Xuhua
|
| Abstract: |
| Annotated logic is one of the paraconsistent logics.The entailments in annotated logic are and |≈. Both of them are paraconsistent, and can treat any set of formulae, either consistent or not, in a uniform way. is monotonic, it has a resolution based sound and complete proof procedure, but some rational inferences of the classical logic, such as modus ponens, are no longer valid under it.|≈ is nonmonotonic. The classical inferences hold true under it when there is no contradiction. But no satisfactory proof theory for |≈ has been given. This paper will propose sound and complete decision Tableaux for and |≈ respectively. |
| Key words: Annotated logic tableaux preferential entailment paraconsistent logic. |
