اشترك بالحزمة الذهبية واحصل على وصول غير محدود شمرا أكاديميا
تسجيل مستخدم جديدHilbert-Post completeness for the state and the exception effects
94
0
0.0
(
0
)
نشر من قبل
Jean-Guillaume Dumas
تاريخ النشر
2015
مجال البحث
الهندسة المعلوماتية
والبحث باللغة
English
تأليف
Jean-Guillaume Dumas
اسأل ChatGPT حول البحث
ﻻ يوجد ملخص باللغة العربية
In this paper, we present a novel framework for studying the syntactic completeness of computational effects and we apply it to the exception effect. When applied to the states effect, our framework can be seen as a generalization of Pretnars work on this subject. We first introduce a relative notion of Hilbert-Post completeness, well-suited to the composition of effects. Then we prove that the exception effect is relatively Hilbert-Post complete, as well as the core language which may be used for implementing it; these proofs have been formalized and checked with the proof assistant Coq.
قيم البحث
اقرأ أيضاً
This paper shows an application of Bloom and Esiks iteration algebras to model graph data in a graph database query language. About twenty years ago, Buneman et al. developed a graph database query language UnQL on the top of a functional meta-langua
ge UnCAL for describing and manipulating graphs. Recently, the functional programming community has shown renewed interest in UnCAL, because it provides an efficient graph transformation language which is useful for various applications, such as bidirectional computation. However, no mathematical semantics of UnQL/UnCAL graphs has been developed. In this paper, we give an equational axiomatisation and algebraic semantics of UnCAL graphs. The main result of this paper is to prove that completeness of our equational axioms for UnCAL for the original bisimulation of UnCAL graphs via iteration algebras. Another benefit of algebraic semantics is a clean characterisation of structural recursion on graphs using free iteration algebra.
This paper exhibits a general and uniform method to prove completeness for certain modal fixpoint logics. Given a set Gamma of modal formulas of the form gamma(x, p1, . . ., pn), where x occurs only positively in gamma, the language Lsharp (Gamma) is
obtained by adding to the language of polymodal logic a connective sharp_gamma for each gamma epsilon. The term sharp_gamma (varphi1, . . ., varphin) is meant to be interpreted as the least fixed point of the functional interpretation of the term gamma(x, varphi 1, . . ., varphi n). We consider the following problem: given Gamma, construct an axiom system which is sound and complete with respect to the concrete interpretation of the language Lsharp (Gamma) on Kripke frames. We prove two results that solve this problem. First, let Ksharp (Gamma) be the logic obtained from the basic polymodal K by adding a Kozen-Park style fixpoint axiom and a least fixpoint rule, for each fixpoint connective sharp_gamma. Provided that each indexing formula gamma satisfies the syntactic criterion of being untied in x, we prove this axiom system to be complete. Second, addressing the general case, we prove the soundness and completeness of an extension K+ (Gamma) of K_sharp (Gamma). This extension is obtained via an effective procedure that, given an indexing formula gamma as input, returns a finite set of axioms and derivation rules for sharp_gamma, of size bounded by the length of gamma. Thus the axiom system K+ (Gamma) is finite whenever Gamma is finite.
It is well known that the resolution method (for propositional logic) is complete. However, completeness proofs found in the literature use an argument by contradiction showing that if a set of clauses is unsatisfiable, then it must have a resolution
refutation. As a consequence, none of these proofs actually gives an algorithm for producing a resolution refutation from an unsatisfiable set of clauses. In this note, we give a simple and constructive proof of the completeness of propositional resolution which consists of an algorithm together with a proof of its correctness.
This paper poses that transition systems constitute a good model of distributed systems only in combination with a criterion telling which paths model complete runs of the represented systems. Among such criteria, progress is too weak to capture rele
vant liveness properties, and fairness is often too strong; for typical applications we advocate the intermediate criterion of justness. Previously, we proposed a definition of justness in terms of an asymmetric concurrency relation between transitions. Here we define such a concurrency relation for the transition systems associated to the process algebra CCS as well as its extensions with broadcast communication and signals, thereby making these process algebras suitable for capturing liveness properties requiring justness.
Existing work on theorem proving for the assertion language of separation logic (SL) either focuses on abstract semantics which are not readily available in most applications of program verification, or on concrete models for which completeness is no
t possible. An important element in concrete SL is the points-to predicate which denotes a singleton heap. SL with the points-to predicate has been shown to be non-recursively enumerable. In this paper, we develop a first-order SL, called FOASL, with an abstracted version of the points-to predicate. We prove that FOASL is sound and complete with respect to an abstract semantics, of which the standard SL semantics is an instance. We also show that some reasoning principles involving the points-to predicate can be approximated as FOASL theories, thus allowing our logic to be used for reasoning about concrete program verification problems. We give some example theories that are sound with respect to different variants of separation logics from the literature, including those that are incompatible with Reynoldss semantics. In the experiment we demonstrate our FOASL based theorem prover which is able to handle a large fragment of separation logic with heap semantics as well as non-standard semantics.
سجل دخول لتتمكن من نشر تعليقات
التعليقات
جاري جلب التعليقات
سجل دخول لتتمكن من متابعة معايير البحث التي قمت باختيارها
