共查询到20条相似文献,搜索用时 15 毫秒
1.
2.
Jan von Plato 《Mathematical Logic Quarterly》2003,49(5):435-443
Gentzen's “Untersuchungen” [1] gave a translation from natural deduction to sequent calculus with the property that normal derivations may translate into derivations with cuts. Prawitz in [8] gave a translation that instead produced cut‐free derivations. It is shown that by writing all elimination rules in the manner of disjunction elimination, with an arbitrary consequence, an isomorphic translation between normal derivations and cut‐free derivations is achieved. The standard elimination rules do not permit a full normal form, which explains the cuts in Gentzen's translation. Likewise, it is shown that Prawitz' translation contains an implicit process of cut elimination. 相似文献
3.
4.
We consider propositional dynamic logic for agents. For this logic, we present a sequent calculus with a restricted cut rule and prove the soundness and completeness for the calculus. 相似文献
5.
J. Sakalauskaite 《Lithuanian Mathematical Journal》2005,45(2):217-224
We consider a propositional dynamic logic for agents with interactions such as known commitment, no learning, and perfect recall. For this logic, we present a sequent calculus with a restricted cut rule and prove the soundness and completeness for the calculus.__________Published in Lietuvos Matematikos Rinkinys, Vol. 45, No. 2, pp. 261–269, April–June, 2005. 相似文献
6.
7.
基于命题逻辑公式之间相似度的概念,在经典命题逻辑系统中提出了两种近似推理模式,得到了它们的一些基本性质。讨论了这两种推理模式与经典推理模式之间的关系。此外,当理论Γ有限时,本文分别给出Γ在α程度上近似推出公式A和理论Σ的充要条件。最后,我们给出公式A与有限理论Γ的结论集D(Γ)之间距离的计算公式。 相似文献
8.
Rosalie Iemhoff 《Annals of Pure and Applied Logic》2019,170(11):102711
This paper presents a uniform and modular method to prove uniform interpolation for several intermediate and intuitionistic modal logics. The proof-theoretic method uses sequent calculi that are extensions of the terminating sequent calculus for intuitionistic propositional logic. It is shown that whenever the rules in a calculus satisfy certain structural properties, the corresponding logic has uniform interpolation. It follows that the intuitionistic versions of and (without the diamond operator) have uniform interpolation. It also follows that no intermediate or intuitionistic modal logic without uniform interpolation has a sequent calculus satisfying those structural properties, thereby establishing that except for the seven intermediate logics that have uniform interpolation, no intermediate logic has such a sequent calculus. 相似文献
9.
R. Alonderis 《Lithuanian Mathematical Journal》2008,48(2):123-136
The paper deals with a coding method for a sequent calculus of the propositional logic. The method is based on the sequent
calculus. It allows us to determine if a formula is derivable in the calculus without constructing a derivation tree. The
main advantage of the coding method is its compactness in comparison with derivation trees of the sequent calculus. The coding
method can be used as a decision procedure for the propositional logic. 相似文献
10.
11.
设Ω是全体从R0-代数M到R0单位区间[0,1]的同态之集,μ是Ω上的一概率测度。引进M上的元素的尺寸和元素对间的相似度,然后在M上建立了伪距离。作为应用,将距离R0-代数理论应用到命题逻辑的近似推理理论。 相似文献
12.
以真度为基础,给出二值命题逻辑系统中基于前提信息的相似度和伪距离的概念以及伪距离的真度表示式,对二值命题逻辑中具有前提信息的近似推理问题进行讨论. 相似文献
13.
J. Sakalauskaitė 《Lithuanian Mathematical Journal》2006,46(3):347-355
We consider logic of knowledge and past time. This logic involves the discrete-time linear temporal operators next, until, weak yesterday, and since. In addition, it contains an indexed set of unary modal operators agent i knows.We consider the semantic constraint of the unique initial states for this logic. For the logic, we present a sequent calculus
with a restricted cut rule. We prove the soundness and completeness of the sequent calculus presented. We prove the decidability
of provability in the considered calculus as well. So, this calculus can be used as a basis for automated theorem proving.
The proof method for the completeness can be used to construct complete sequent calculi with a restricted cut rule for this
logic with other semantical constraints as well.
Published in Lietuvos Matematikos Rinkinys, Vol. 46, No. 3, pp. 427–437, July–September, 2006. 相似文献
14.
R. Alonderis 《Lithuanian Mathematical Journal》2005,45(1):1-15
We consider classical, multisuccedent intuitionistic, and intuitionistic sequent calculi for propositional likelihood logic. We prove the admissibility of structural rules and cut rule, invertibility of rules, correctness of the calculi, and completeness of the classical calculus with respect to given semantics.__________Published in Lietuvos Matematikos Rinkinys, Vol. 45, No. 1, pp. 3–21, January–March, 2005. 相似文献
15.
Kentaro Kikuchi 《Mathematical Logic Quarterly》2002,48(1):87-92
We introduce a dual‐context style sequent calculus which is complete with respectto Kripke semantics where implication is interpreted as strict implication in the modal logic K. The cut‐elimination theorem for this calculus is proved by a variant of Gentzen's method. 相似文献
16.
二值命题逻辑系统中理论Г的带误差结论集是近似推理研究的基本对象,对其结构进行分析是近似推理研究中需要解决的问题。通过公式是有限理论Г的带误差结论的充要条件,利用集合划分方法,对有限理论Г的带误差结论集分别基于真度相等关系和逻辑等价关系进行分类,得到了基于两类等价关系的包含等价类个数和代表元表示形式的分类定理,进一步体现了二值命题逻辑系统近似推理研究中理论Г的带误差结论集的特征。 相似文献
17.
18.
Wojciech Buszkowski 《Mathematical Logic Quarterly》2003,49(5):467-474
Compact Bilinear Logic (CBL), introduced by Lambek [14], arises from the multiplicative fragment of Noncommutative Linear Logic of Abrusci [1] (also called Bilinear Logic in [13]) by identifying times with par and 0 with 1. In this paper, we present two sequent systems for CBL and prove the cut‐elimination theorem for them. We also discuss a connection between cut‐elimination for CBL and the Switching Lemma from [14]. 相似文献
19.
Meghdad Ghari 《Annals of Pure and Applied Logic》2017,168(1):72-111
Justification logics are modal-like logics that provide a framework for reasoning about justifications. This paper introduces labeled sequent calculi for justification logics, as well as for combined modal-justification logics. Using a method due to Sara Negri, we internalize the Kripke-style semantics of justification and modal-justification logics, known as Fitting models, within the syntax of the sequent calculus to produce labeled sequent calculi. We show that all rules of these systems are invertible and the structural rules (weakening and contraction) and the cut rule are admissible. Soundness and completeness are established as well. The analyticity for some of our labeled sequent calculi are shown by proving that they enjoy the subformula, sublabel and subterm properties. We also present an analytic labeled sequent calculus for based on Artemov–Fitting models. 相似文献
20.
Let LB be a sequent calculus of the first-order classical temporal logic TB with time gaps. Let, further, LBJ be the intuitionistic counterpart of LB. In this paper, we consider conditions under which a sequent is derivable in the calculus LBJ if and only if it is derivable in the calculus LB. Such conditions are defined for sequents with one formula in the succedent (purely Glivenko -classes) and for sequents with the empty succedent (Glivenko -classes). 相似文献