اشترك بالحزمة الذهبية واحصل على وصول غير محدود شمرا أكاديميا
تسجيل مستخدم جديدA classical-logic view of a paraconsistent logic
123
0
0.0
(
0
)
تأليف
C. A. Middelburg
اسأل ChatGPT حول البحث
ﻻ يوجد ملخص باللغة العربية
This paper is concerned with the first-order paraconsistent logic LPQ$^{supset,mathsf{F}}$. A sequent-style natural deduction proof system for this logic is presented and, for this proof system, both a model-theoretic justification and a logical justification by means of an embedding into first-order classical logic is given. For no logic that is essentially the same as LPQ$^{supset,mathsf{F}}$, a natural deduction proof system is currently available in the literature. The given embedding provides both a classical-logic explanation of this logic and a logical justification of its proof system. The major properties of LPQ$^{supset,mathsf{F}}$ are also treated.
قيم البحث
اقرأ أيضاً
Action logic is the algebraic logic (inequational theory) of residuated Kleene lattices. This logic involves Kleene star, axiomatized by an induction scheme. For a stronger system which uses an $omega$-rule instead (infinitary action logic) Buszkowsk
i and Palka (2007) have proved $Pi_1^0$-completeness (thus, undecidability). Decidability of action logic itself was an open question, raised by D. Kozen in 1994. In this article, we show that it is undecidable, more precisely, $Sigma_1^0$-complete. We also prove the same complexity results for all recursively enumerable logics between action logic and infinitary action logic; for fragments of those only one of the two lattice (additive) connectives; for action logic extended with the law of distributivity.
In this paper we provide two new semantics for proofs in the constructive modal logics CK and CD. The first semantics is given by extending the syntax of combinatorial proofs for propositional intuitionistic logic, in which proofs are factorised in a
linear fragment (arena net) and a parallel weakening-contraction fragment (skew fibration). In particular we provide an encoding of modal formulas by means of directed graphs (modal arenas), and an encoding of linear proofs as modal arenas equipped with vertex partitions satisfying topological criteria. The second semantics is given by means of winning innocent strategies of a two-player game over modal arenas. This is given by extending the Heijltjes-Hughes-Stra{ss}burger correspondence between intuitionistic combinatorial proofs and winning innocent strategies in a Hyland-Ong arena. Using our first result, we provide a characterisation of winning strategies for games on a modal arena corresponding to proofs with modalities.
Description logics are knowledge representation languages that have been designed to strike a balance between expressivity and computational tractability. Many different description logics have been developed, and numerous computational problems for
these logics have been studied for their computational complexity. However, essentially all complexity analyses of reasoning problems for description logics use the one-dimensional framework of classical complexity theory. The multi-dimensional framework of parameterized complexity theory is able to provide a much more detailed image of the complexity of reasoning problems. In this paper we argue that the framework of parameterized complexity has a lot to offer for the complexity analysis of description logic reasoning problems---when one takes a progressive and forward-looking view on parameterized complexity tools. We substantiate our argument by means of three case studies. The first case study is about the problem of concept satisfiability for the logic ALC with respect to nearly acyclic TBoxes. The second case study concerns concept satisfiability for ALC concepts parameterized by the number of occurrences of union operators and the number of occurrences of full existential quantification. The third case study offers a critical look at data complexity results from a parameterized complexity point of view. These three case studies are representative for the wide range of uses for parameterized complexity methods for description logic problems.
Short-circuit evaluation denotes the semantics of propositional connectives in which the second argument is evaluated only if the first argument does not suffice to determine the value of the expression. Free short-circuit logic is the equational log
ic in which compound statements are evaluated from left to right, while atomic evaluations are not memorised throughout the evaluation, i.e., evaluations of distinct occurrences of an atom in a compound statement may yield different truth values. We provide a simple semantics for free SCL and an independent axiomatisation. Finally, we discuss evaluation strategies, some other SCLs, and side effects.
We propose a model of the substructural logic of Bunched Implications (BI) that is suitable for reasoning about quantum states. In our model, the separating conjunction of BI describes separable quantum states. We develop a program logic where pre- a
nd post-conditions are BI formulas describing quantum states -- the program logic can be seen as a counterpart of separation logic for imperative quantum programs. We exercise the logic for proving the security of quantum one-time pad and secret sharing, and we show how the program logic can be used to discover a flaw in Google Cirqs tutorial on the Variational Quantum Algorithm (VQA).
سجل دخول لتتمكن من نشر تعليقات
التعليقات
جاري جلب التعليقات
سجل دخول لتتمكن من متابعة معايير البحث التي قمت باختيارها
