Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userOn sufficient conditions for expressibility of constants in the 4-valued extension of the propositional provability logic $GL$
211
0
0.0
(
0
)
Added by
Andrei Rusu
Publication date
2013
fields
Informatics Engineering
and research's language is
English
Authors
Andrei Rusu
Ask ChatGPT about the research
No Arabic abstract
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.
rate research
Read More
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 that 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.
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 existentially $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).
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
