Questions tagged [logical-validity]
The logical-validity tag has no usage guidance.
20
questions
3
votes
1
answer
86
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 ...
CommunityBot
- 1
0
votes
1
answer
327
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 ...
- 852
0
votes
0
answers
38
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 ...
- 113
1
vote
0
answers
96
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 ...
1
vote
1
answer
100
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 ...
- 235
0
votes
0
answers
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
1
answer
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 ...
- 22.1k
0
votes
0
answers
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 ...
- 162
5
votes
2
answers
259
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 ...
- 3,276
0
votes
0
answers
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 ...
- 173
1
vote
1
answer
166
views
Showing the following sequents are not valid
$\lnot \forall x P(x) \models \forall x \lnot P(x)$
$P(x) : x$ is divisible by 2
or $P(x) : x$ is a dog.
or $P(x) can be anything.
I want to show the following sequents are not valid ..Isn't the ...
- 9,837
1
vote
1
answer
57
views
Verifying execution of code in trustless environment
Let us assume I have a Program P running on remote computer generating output O. Without trusting the remote environment and not having to verify the output O, is there is a way to validate that ...
D.W.♦
- 159k
3
votes
1
answer
186
views
Contingent sentences can always be true
I have a question about contingent sentences. To my knowledge, contingent sentences are sentences that are neither tautologies nor contradictions.
In a textbook I read that a sentence might always be ...
- 261
-1
votes
1
answer
90
views
Horn clause for the following formula
Let be
$$F=A\land (\neg A\lor B)\land(A\lor \neg C)\land(\neg A\lor\neg B\lor D)\land(\neg A\lor\neg B\lor\neg C)$$
a formula. Is $F$ satisfiable?
Well, firstly, I've put $F$ into another form:
$$...
- 147
1
vote
0
answers
250
views
Proving the following chain of implications
I'm struggling with a proof in the text for my logic course, and I'm wondering if someone could offer a hint or some help. The question is basically as follows. Show that if the decision problem for ...
- 115
0
votes
1
answer
77
views
If $F$ is valid then $F \cup \{res(C_1,C_2,A_i)\}$ is valid
I have to prove the following problem in propositional logic:
Let $F$ be a set of clauses and let $F' = F \cup \{res(C_1,C_2,A_i)\}$ be the extension of $F$ by a resolvent of some clauses $C_1,C_2 \...
- 19.5k
1
vote
2
answers
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 ...
- 72.4k
5
votes
1
answer
2k
views
Validity of predicate logic formulas
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 ...
- 16.1k
2
votes
1
answer
374
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 ...
- 72.4k
2
votes
3
answers
530
views
Is switching quantifiers allowed in this instance?
In Logic In Computer Science (2nd Edition - Michael Huth and Mark Ryan), exercise 2.4.12.k is the following:
For each of the formulas of predicate logic below, either find a model which
does not ...
