اشترك بالحزمة الذهبية واحصل على وصول غير محدود شمرا أكاديميا
تسجيل مستخدم جديدCompleteness of Hoare Logic over Nonstandard Models
206
0
0.0
(
0
)
اسأل ChatGPT حول البحث
ﻻ يوجد ملخص باللغة العربية
The nonstandard approach to program semantics has successfully resolved the completeness problem of Floyd-Hoare logic. The kno
قيم البحث
اقرأ أيضاً
The general completeness problem of Hoare logic relative to the standard model $N$ of Peano arithmetic has been studied by Cook, and it allows for the use of arbitrary arithmetical formulas as assertions. In practice, the assertions would be simple a
rithmetical formulas, e.g. of a low level in the arithmetical hierarchy. In addition, we find that, by restricting inputs to $N$, the complexity of the minimal assertion theory for the completeness of Hoare logic to hold can be reduced. This paper further studies the completeness of Hoare Logic relative to $N$ by restricting assertions to subclasses of arithmetical formulas (and by restricting inputs to $N$). Our completeness results refine Cooks result by reducing the complexity of the assertion theory.
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.
We present a formal system for proving the partial correctness of a single-pass instruction sequence as considered in program algebra by decomposition into proofs of the partial correctness of segments of the single-pass instruction sequence concerne
d. The system is similar to Hoare logics, but takes into account that, by the presence of jump instructions, segments of single-pass instruction sequences may have multiple entry points and multiple exit points. It is intended to support a sound general understanding of the issues with Hoare-like logics for low-level programming languages.
Coalition logic is one of the most popular logics for multi-agent systems. While epistemic extensions of coalition logic have received much attention, existence of their complete axiomatisations has so far been an open problem. In this paper we settl
e several of those problems. We prove completeness for epistemic coalition logic with common knowledge, with distributed knowledge, and with both common and distributed knowledge, respectively.
Algebraic logic studies algebraic theories related to proposition and first-order logic. A new algebraic approach to first-order logic is sketched in this paper. We introduce the notion of a quantifier theory, which is a functor from the category of
a monad of sets to the category of Boolean algebras, together with a uniquely determined system of quantifiers. A striking feature of this approach is that Cayleys Completeness Theorem and Godels Completeness Theorem can be stated and proved in a much simpler fashion for quantifier theories. Both theorems are due to Halmos for polyadic algebras. We also present a simple transparent treatment of ultraproducts of models of a quantifier theory.
سجل دخول لتتمكن من نشر تعليقات
التعليقات
جاري جلب التعليقات
سجل دخول لتتمكن من متابعة معايير البحث التي قمت باختيارها
