اشترك بالحزمة الذهبية واحصل على وصول غير محدود شمرا أكاديميا
تسجيل مستخدم جديدRelating Reasoning Methodologies in Linear Logic and Process Algebra
171
0
0.0
(
0
)
تأليف
Yuxin Deng
اسأل ChatGPT حول البحث
ﻻ يوجد ملخص باللغة العربية
We show that the proof-theoretic notion of logical preorder coincides with the process-theoretic notion of contextual preorder for a CCS-like calculus obtained from the formula-as-process interpretation of a fragment of linear logic. The argument makes use of other standard notions in process algebra, namely a labeled transition system and a coinductively defined simulation relation. This result establishes a connection between an approach to reason about process specifications and a method to reason about logic specifications.
قيم البحث
اقرأ أيضاً
This paper concerns the relation between process algebra and Hoare logic. We investigate the question whether and how a Hoare logic can be used for reasoning about how data change in the course of a process when reasoning equationally about that proc
ess. We introduce an extension of ACP (Algebra of Communicating Processes) with features that are relevant to processes in which data are involved, present a Hoare logic for the processes considered in this process algebra, and discuss the use of this Hoare logic as a complement to pure equational reasoning with the equational axioms of the process algebra.
Linear Logic was introduced by Girard as a resource-sensitive refinement of classical logic. It turned out that full propositional Linear Logic is undecidable (Lincoln, Mitchell, Scedrov, and Shankar) and, hence, it is more expressive than (modalized
) classical or intuitionistic logic. In this paper we focus on the study of the simplest fragments of Linear Logic, such as the one-literal and constant-only fragments (the latter contains no literals at all). Here we demonstrate that all these extremely simple fragments of Linear Logic (one-literal, $bot$-only, and even unit-only) are exactly of the same expressive power as the corresponding fu
The paper introduces a knowledge representation language that combines the event calculus with description logic in a logic programming framework. The purpose is to provide the user with an expressive language for modelling and analysing systems that
evolve over time. The approach is exemplified with the logic programming language as implemented in the Fusemate system. The paper extends Fusemates rule language with a weakly DL-safe interface to the description logic $cal ALCIF$ and adapts the event calculus to this extended language. This way, time-stamped ABoxes can be manipulated as fluents in the event calculus. All that is done in the frame of Fusemates concept of stratification by time. The paper provides conditions for soundness and completeness where appropriate. Using an elaborated example it demonstrates the interplay of the event calculus, description logic and logic programming rules for computing possible models as plausible explanations of the current state of the modelled system.
In the case of multi-threading as found in contemporary programming languages, parallel processes are interleaved according to what is known as a process-scheduling policy in the field of operating systems. In a previous paper, we extend ACP with thi
s form of interleaving. In the current paper, we do so with the variant of ACP known as ACP$_epsilon$. The choice of ACP$_epsilon$ stems from the need to cover more process-scheduling policies. We show that a process-scheduling policy supporting mutual exclusion of critical subprocesses is now covered.
We first present a probabilistic version of ACP that rests on the principle that probabilistic choices are always resolved before choices involved in alternative composition and parallel composition are resolved and then extend this probabilistic ver
sion of ACP with a form of interleaving in which parallel processes are interleaved according to what is known as a process-scheduling policy in the field of operating systems. We use the term strategic interleaving for this more constrained form of interleaving. The extension covers probabilistic process-scheduling policies.
سجل دخول لتتمكن من نشر تعليقات
التعليقات
جاري جلب التعليقات
سجل دخول لتتمكن من متابعة معايير البحث التي قمت باختيارها
