# Questions tagged [logical-validity]

The tag has no usage guidance.

20 questions
Filter by
Sorted by
Tagged with
263 views

### How can I prove that LTL formula is valid?

I do not know with which technique i can prove if a LTL forumula is valid. Let's say we have for example this one: ¬q U(¬p ∧ ¬q) → ¬Gp. How can prove if this valid or not? (should be true in any state ...
34 views

### Specific quantifier elimination for real algebraic numbers

It is well-known that the theory of (first-order) real arithmetic, $\mathcal{T}_{\mathbb{R}}$, is decidable, both on its linear and non-linear (a.k.a field) fragments, since Tarski-Seindenberg proved ...
1 vote
91 views

### SMT validity solvers/ quantifier elimination in Ocaml

I am working on my own expression package in Ocaml and have to perform both validity queries and quantifier elimination. I have already implemented Cooper's procedure (for Presburger and Linear ...
33 views

### Space time diagram for debugging in message passing parallel programs?

I was asked in the test to draw a Spacetime diagram for debugging in message-passing parallel programs, I want to know is this even a valid question?
1 vote
98 views

### Incomplete definition of function- first order logic

Let $\Sigma=\{c,f^1,R_1^2,...,R_k^2\}$ where $c$ is constant, $f$ is one argument function, and $R_i$ are binary relations. Let $\Sigma_2=\{c',g^2,R_1'^1,...,R_k'^1\}$ where $c'$ is constant, $g$ is ...
82 views

### equivalence of validity above different alphabet

Given the next alphabets: $\,\,\Sigma_1=\{R^2,P^1,=^2\}\,\,,\Sigma_2=\{c,f^1,=^2\}.$ Prove of Disprove: There's exists an algorithm, that given formula $A$ above $\Sigma_2$, builds formula $A'$ above ...
1 vote
23 views

### Consequences of a language that hides his lower level rappresentations

I know it's a silly scenario but I wolud like to know if it's relevant and maybe there are some sort of theory/studies on it or it's merely a non-sense situation. Immagine a language much close to a ...
39 views

### Calculus methods and computability

We know about calculability of a function or computability. We looks for the ability to solve a specific problem / compute a function with calculus method. But if we define a calculus method, is ...
257 views

### Undecidable predicate logic is decidable by people?

Logic in computer science (By Michael Huth,Mark Ryan, second edition, page 132) says Every φ can, in principle, be discovered to be valid or not, if you are prepared to work arbitrarily hard at ...
31 views

### Show the Invalidity of the sequence

∃x (P(x) → Q(x)), ∃x P(x) ⊨ ∃x Q(x) I am trying to find the invalidity of the following sequents. A = Set of natural number P(x) : x is odd Q(x) : x is not divisible by 2 What i don't understand ...
1 vote
162 views

1 vote
130 views

### Using the rules of inferences

I know the rules of inferences and logical equivalence but I cannot seem to validate this argument. I rewrote the first premise as $\neg p\vee q$ other from that I am stuck. Any help will be ...
372 views

### definition of formula validity

I read in some sources that valid formulas are tautologies (valid under every evaluation). In the others, I read that these are formulas that have conclusions true when premises are true. Are these ...
The following predicate logic formula is invalid (i.e. not a tautology): $\Bigl[\forall x \,\exists y {\,.\,} P(x,y)\Bigr] \implies \Bigl[\exists y \, \forall x {\,.\,} P(x,y)\Bigr]$ Which of the ...