论文标题
基于邻里语义的优先条件逻辑的统一标记的骨子
Uniform labelled calculi for preferential conditional logics based on neighbourhood semantics
论文作者
论文摘要
研究了由Burgess引入的优先条件逻辑PCL及其扩展。首先，提出了基于邻里模型的自然语义，该语义概括了刘易斯的反事实逻辑模型。直接证明了PCL及其相对于此类模型的稳健性和完整性。然后引入了所有家族逻辑的标记的序列计算。该结石是模块化的，具有标准的证明理论特性，其中最重要的是削减的可接受性，它需要句法的结石证明。通过采用一般策略，从根本上的证明搜索终止，从而为PCL及其扩展提供了决策程序。最后，建立了结石的语义完整性：从失败的证明尝试中的有限分支开始，可以提取根序列的有限反模型。后一个结果给出了所有考虑的逻辑的有限模型属性的建设性证明。
The preferential conditional logic PCL, introduced by Burgess, and its extensions are studied. First, a natural semantics based on neighbourhood models, which generalise Lewis' sphere models for counterfactual logics, is proposed. Soundness and completeness of PCL and its extensions with respect to this class of models are proved directly. Labelled sequent calculi for all logics of the family are then introduced. The calculi are modular and have standard proof-theoretical properties, the most important of which is admissibility of cut, that entails a syntactic proof of completeness of the calculi. By adopting a general strategy, root-first proof search terminates, thereby providing a decision procedure for PCL and its extensions. Finally, the semantic completeness of the calculi is established: from a finite branch in a failed proof attempt it is possible to extract a finite countermodel of the root sequent. The latter result gives a constructive proof of the finite model property of all the logics considered.
