ترغب بنشر مسار تعليمي؟ اضغط هنا

On sufficient conditions for expressibility of constants in the 4-valued extension of the propositional provability logic $GL$

200   0   0.0 ( 0 )
 نشر من قبل Andrei Rusu
 تاريخ النشر 2013
  مجال البحث الهندسة المعلوماتية
والبحث باللغة English
 تأليف Andrei Rusu




اسأل ChatGPT حول البحث

In the present paper we consider the simplest non-classical extension $GL4$ of the well-known propositional provability logic $GL$ together with the notion of expressibility of formulas in a logic proposed by A. V. Kuznetsov. Conditions for expressibility of constants in the 4-valued extension $Lmathfrak{B}_2$ of $GL$ are found out, which were first announced in a authors paper in 1996.



قيم البحث

اقرأ أيضاً

We study counting propositional logic as an extension of propositional logic with counting quantifiers. We prove that the complexity of the underlying decision problem perfectly matches the appropriate level of Wagners counting hierarchy, but also th at the resulting logic admits a satisfactory proof-theoretical treatment. From the latter, a type system for a probabilistic lambda-calculus is derived in the spirit of the Curry-Howard correspondence, showing the potential of counting propositional logic as a useful tool in several fields of theoretical computer science.
The logic of equality with uninterpreted functions (EUF) provides a means of abstracting the manipulation of data by a processor when verifying the correctness of its control logic. By reducing formulas in this logic to propositional formulas, we can apply Boolean methods such as Ordered Binary Decision Diagrams (BDDs) and Boolean satisfiability checkers to perform the verification. We can exploit characteristics of the formulas describing the verification conditions to greatly simplify the propositional formulas generated. In particular, we exploit the property that many equations appear only in positive form. We can therefore reduce the set of interpretations of the function symbols that must be considered to prove that a formula is universally valid to those that are ``maximally diverse. We present experimental results demonstrating the efficiency of this approach when verifying pipelined processors using the method proposed by Burch and Dill.
We characterise the sentences in Monadic Second-order Logic (MSO) that are over finite structures equivalent to a Datalog program, in terms of an existential pebble game. We also show that for every class C of finite structures that can be expressed in MSO and is closed under homomorphisms, and for all integers l,k, there exists a *canonical* Datalog program Pi of width (l,k), that is, a Datalog program of width (l,k) which is sound for C (i.e., Pi only derives the goal predicate on a finite structure A if A is in C) and with the property that Pi derives the goal predicate whenever *some* Datalog program of width (l,k) which is sound for C derives the goal predicate. The same characterisations also hold for Guarded Second-order Logic (GSO), which properly extends MSO. To prove our results, we show that every class C in GSO whose complement is closed under homomorphisms is a finite union of constraint satisfaction problems (CSPs) of countably categorical structures.
116 - Roy Mennicke 2013
The model checking problem for propositional dynamic logic (PDL) over message sequence charts (MSCs) and communicating finite state machines (CFMs) asks, given a channel bound $B$, a PDL formula $varphi$ and a CFM $mathcal{C}$, whether every existent ially $B$-bounded MSC $M$ accepted by $mathcal{C}$ satisfies $varphi$. Recently, it was shown that this problem is PSPACE-complete. In the present work, we consider CRPDL over MSCs which is PDL equipped with the operators converse and repeat. The former enables one to walk back and forth within an MSC using a single path expression whereas the latter allows to express that a path expression can be repeated infinitely often. To solve the model checking problem for this logic, we define message sequence chart automata (MSCAs) which are multi-way alternating parity automata walking on MSCs. By exploiting a new concept called concatenation states, we are able to inductively construct, for every CRPDL formula $varphi$, an MSCA precisely accepting the set of models of $varphi$. As a result, we obtain that the model checking problem for CRPDL and CFMs is still in PSPACE.
In this short note we address the issue of expressing norms (such as obligations and prohibitions) in temporal logic. In particular, we address the argument from [Governatori 2015] that norms cannot be expressed in Linear Time Temporal Logic (LTL).
التعليقات
جاري جلب التعليقات جاري جلب التعليقات
mircosoft-partner

هل ترغب بارسال اشعارات عن اخر التحديثات في شمرا-اكاديميا