Questions tagged [propositional-logic]
The propositional-logic tag has no usage guidance.
208 questions
0
votes
0
answers
25
views
□(P→ □Q) → P → □Q validity in Propositional Temporal Logic
How can i analyse the validity in Propositional Temporal Logic (PTL) of this formula, Is that necessary to use the Kripke structure?
- 11
0
votes
2
answers
50
views
How to interpret "implication holds" or "implication doesn't hold"?
Lets say we have a sentence, "If it is raining, then I will take the cab".
Let's say
$$
p: \text{It is raining} \\
q: \text{I will take the cab}
$$
In this if it is actually raining (...
- 208
0
votes
1
answer
50
views
How would I prove implications of this structure?
Consider the following to prove: $(A \implies B) \implies (C \implies D)$
Could this be proved by assuming A then proving B, then using A and B to prove C, then using A, B and C to prove D? or would ...
- 173
2
votes
0
answers
42
views
Satisfiability of a boolean formula with two occurrences of each variable with a special ordering
I am interested in the complexity of a special case of the boolean satisfiability problem:
We are given a boolean formula, consisting only of the logical operators $\land$ and $\lor$ (that can be ...
- 161
0
votes
0
answers
24
views
Finding a common variable value among all SAT solutions
Let $F$ be a boolean formula on $n$ variables $x_1, \cdots, x_n$. $\textbf{SAT}(F)$ asks whether there exists an assignment of truth values to variables under which $F$ is true. I'm curious about ...
0
votes
0
answers
58
views
Why can't we say that P=NP if we have an infinite text file with solution for every possible SAT combination?
I believe that I have a misunderstanding in the P=NP problem while I was thinking of how can it be proved in a non-constructive manner.
We know that we can build an infinitely large text file with ...
- 1
2
votes
3
answers
1k
views
Does Either...Or means Exclusive Or or Inclusive Or?
Let's take a compound propositions
Either it is below freezing or it is snowing.
Now if,
$p$: it is below freezing
$q$: it is snowing
Question Link: https://gateoverflow.in/42720/kenneth-rosen-...
- 208
2
votes
1
answer
224
views
Tseitin formula on 2-connected graph
How can we prove that for $\\\\$ every $\\\\$ 2-connected graph G with an odd number of vertices, the unsatisfiable Tseitin formula for it is minimally unsatisfiable, that is, if we remove even a ...
user167124
0
votes
1
answer
140
views
Resolution on weakening rule by derived clause
How to prove that every clause that is implied by the input formula (learned or not) can be derived using resolution with weakening rule:
$\frac{C}
{C \vee D}$
(A clause $C$ is implied by $F$ if for ...
user150715
2
votes
2
answers
422
views
I've heard that it isn't possible to encode product types and sum types in a simply typed lambda calculus, but it seems for me that it's false
Of course, it isn't possible to construct them directly since we hasn't these type constructors, but only function constructor (arrow). But suppose there are 2 types $A$ and $B$, from which we need to ...
- 109
1
vote
0
answers
39
views
What logical system does hindley-milner correspond to, according to the curry howard correspondence?
If I understand CHC correctly, simply typed lambda calculus corresponds to propositional logic. As HM allows polymorphic definitions by let-expressions, my guess is that it would correspond to a ...
- 36
2
votes
0
answers
25
views
SAT for clauses of the form "At most m out of n are false"
Recall some terminology: Let $\mathsf P$ be a finite set of propositional atoms, and let $\Phi$ be a proposition over $P$ that is generated from $\top$, $\bot$, $\neg$, $\wedge$, and $\vee$. Then:
A ...
- 171
0
votes
2
answers
67
views
Is there a model for the given logical formula, and if not, why?
I'm trying to determine whether there exists a model for the following logical formula: $(p_1 \to (p_2 \lor p_3)) \land(p_2 \to \neg p_3) \land ((p_1 \lor p_3) \to \neg p_2)$. Here's my understanding ...
- 3
1
vote
1
answer
54
views
How big is a formula equivalent to a wff over $n$ variables with $2^n$ subformulas?
Definitions: Let $n \in \mathbb{N}$. If $\alpha$
and $\beta$ are propositional formulas,
then we'll call $\alpha$ and $\beta$ independent if neither implies the other,
or more formally, if $\lnot (\...
- 947
2
votes
0
answers
24
views
Stålmarck's method, can triplets be dropped once they triggered equivalences
In Sheeran, Mary, and Gunnar Stålmarck: A tutorial on Stålmarck’s proof procedure for propositional logic there is an example application of the method to...
- 98
0
votes
0
answers
40
views
Growth of a set of propositional formulas under partial evaluation
Definitions: Let $n \in \mathbb{N}, n \geq 1$. We write $|\alpha|$ to denote the length in characters of an expression $\alpha$ in propositional logic. We define partial evaluation in the normal way ...
- 947
1
vote
1
answer
41
views
Complexity of a Set of Formulas
Notation: We write $|\alpha|$ to denote the length in characters of an expression $\alpha$ in propositional logic.
Consider an expression $\alpha_n$ in disjunctive normal form built from $2n$ ...
- 947
0
votes
2
answers
131
views
Is T V F a tautology?
(Consider $T=true$, $F=false$)
I apologize for the simple question but I'm confused as to what is a tautology and what isn't and I haven't found a clear definition. I think that a tautology is a ...
- 3
2
votes
1
answer
91
views
Sequent calculus and vs comma: $a \land b \implies ...$ vs $a, b \implies ...$
I was reading "Open Logic book", "Sequent Calculus".
Given the fact that all antecedents must hold for at least one succedent to hold, I can't get rid off the impression that using ...
- 123
0
votes
1
answer
147
views
Is any 2-CNF has 2-DNF representation?
I was asked a question whether I could come up with a 2-CNF over several variables that has no 2-DNF representation. However I thought that any CNF can be converted to DNF through some manipulations e....
- 103
1
vote
0
answers
51
views
Application of a formal definition of $max, min$ to evaluate an expression
For an Algorithms course we are studying propositional calculus. As an excercise we are given formal statements which we are to explain in natural language first and then evaluate with specific values....
- 195
0
votes
1
answer
173
views
Is "Bitwise Complement Operator" (~ tilde) distributive?
To be more precise, Is ~(a+b) = ~a + ~b? Here, "~" bitwise NOT operator.
I ran into this question while thinking about ...
- 1
0
votes
2
answers
225
views
My attempt at the "This statement is false" paradox
(I haven't read any literature on this paradox nor am I good at formal proofs, so this is just my intuitive thoughts on the paradox.)
If we assume the statement "This statement is false" as ...
- 1,153
1
vote
1
answer
173
views
Proof that propositional resolution is refutation complete
I am studying theoretical computer science and I am in the part about resolution in propositional calculus. I was reading a theorem (and its proof) that propositional resolution is refutation complete,...
- 310
0
votes
1
answer
34
views
How to get the formal model using propositional logic
Input
There are three chairs (1,2,3) in the same row.
We need to find a seat for three guests (a,b,c).
Constraints
The first guest does not want to be seated next to the third one (neither left nor ...
0
votes
2
answers
54
views
Logical equivalence priority
I have the logical formula
$$
A \Leftrightarrow B \Leftrightarrow C
$$
In order to make the truth table I'm not sure wheither I should interpret it as
$A \Leftrightarrow B \Leftrightarrow C$ or $A \...
0
votes
1
answer
95
views
Logical Consequence - Equivalent Assertions
I have the following slide in my notes and I'm having trouble understanding how the three assertions are equivalent. I understand to a degree how the 2nd and 3rd assertions are equivalent, but the ...
- 9
1
vote
1
answer
84
views
Simple Skolemization Question
Is it correct that, under a certain signature S, two First Order Logic formulae F and G are equisatisfiable if (F is satisfiable under S iff G is satisfiable under S)? But in Skolemization I’m ...
1
vote
0
answers
305
views
Horn Satisfiability is NP Complete, isn't it?
To show that any formal language is NP Complete first it must be showed that this formal language is both in NP and NP Hard.
So to show that Horn Satisfiability is NP Complete first it must be showed ...
-1
votes
2
answers
90
views
Is there a quantifier more powerful than the other to determine FOL connector?
So basically we have 2 types of quantifier in first order logic, they are universal quantifier and existential quantifier. Usually we use implies connector(->) when we have universal quantifier in ...
3
votes
1
answer
84
views
Stalmarck's method: x ≡ x → z, does z have to be true?
I have been researching Ståmarck's method 1. In the paper cited here, some rules are given. Rules are made of triplets (x, y, z) such that:
y $\to$ z $\equiv$ x
where x, y and z are booleans which ...
- 53
-1
votes
1
answer
78
views
Conjuctive Normal Form
Let f(P,Q,R) be the truth-function defined as follows. f(P,Q,R)=1 if and only if
Q and R have different truth-values; or
P and R have the same truth-values.
Choose all formulas that are in conjunctive ...
0
votes
1
answer
210
views
NP-Completeness of SAT with given hamming weight k [duplicate]
I think that the following problem is NP-Complete but I don't have any idea of how doing the reduction.
Input: A propositional formula $\varphi$ and a number $k$.
Output: Yes if exists an valuation $\...
- 115
0
votes
1
answer
93
views
Is it possible to encode contradictory horn clauses without goal clauses?
Intuitively, this seems impossible (because negation is forbidden in the head), but i am not sure.
A naive (and wrong) example is
p :- p
But, this just means
...
- 295
-1
votes
2
answers
103
views
Proof of a logical theorem
Prove that if for every proposition $\psi\left(p_{0}, \ldots, p_{n}, p\right)$ there exists
$\phi\left(p_{0}, \ldots, p_{n}\right)$ in which $\psi\left(p_{0}, \ldots, p_{n}, p\right) \rightarrow\left(\...
- 15
0
votes
2
answers
133
views
Validity of proof by contradiction
I had a doubt in the proof by contradiction technique.
Under this technique, we assume the negation of what we want to prove as true, then show that assuming so generates a contradiction. Since a ...
- 1
2
votes
3
answers
2k
views
Why is SAT based on the CNF?
I have been reading up on Boolean logic and, specifically, the Boolean satisfiability problem. I have seen several people mention that the expression must be converted to conjunctive normal form (CNF) ...
- 133
1
vote
1
answer
168
views
To prove (KB ⊭ S) and (KB ⊭ ¬S) is satisfiable
In question (e), I have to prove: A ≡ (KB ⊭ S) and (KB ⊭ ¬S) is satisfiable, where KB and S are propositional variables. I am not able to follow the solution given in the image above as to why it is ...
- 21
4
votes
1
answer
50
views
Is there a $L$-complete variant of SAT?
Many complete problem of different class of complexity has SAT variant. Like 3-SAT or $k$-SAT is $NP$-complete, Horn-SAT is $P$-complete, 2-SAT is $NL$-complete, and so on. So I was wondering if there ...
- 43
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 ...
- 109
2
votes
2
answers
119
views
Problem with formalism in first order logic
This is a general question in first order logic.
Assume I have alphabet $\Sigma$ that contains one-argument function (among other symbols).
I want a new alphabet, $\Sigma'$, which is the same as the ...
- 109
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 ...
- 109
2
votes
1
answer
693
views
a conjunctive normal form that is a tautology
Are there any examples of CNF formulas that are tautologies?
Such that every clause contains different variables so phrases like (a or not a) are rejected?
- 45
0
votes
0
answers
62
views
Hoare Triple Logic
I'm having trouble understanding the logic behind Hoare Triples. The question asks for the missing value of the precondition {X}
...
1
vote
1
answer
105
views
What is the Number of Possible Nonequivalent Propositions with $P_1, P_2, P_3$ Using $\iff$ Operator?
A multiple choice question asks this:
Number of nonequivalent propositions that only consist of $P_1, P_2, P_3$ and use the $\iff$ logical operator is?$$A)7\text{ }B)8\text{ }C)1\text{ }D)16$$
I am ...
- 59
0
votes
1
answer
27
views
Doubt regarding the implications of a 2-SAT constraint
Consider an example 2-SAT instance with the constraint (x1 ∨ x2).
This CNF has these two implications:
¬x1→x2 and ¬x2→x1.
"They actually mean, if x1 is false then x2 must be true, and if ...
2
votes
1
answer
117
views
Formal Logic - Natural deduction: Problem with assumptions about exists-negation
I'm stuck on how to progress with this proof, despite I have tried, I cannot see the next move.
Given this proof without predicate:
So far what I've accomplished:
My idea is, as I can't see any ...
0
votes
1
answer
602
views
Converting to CNF - Distribution
I am still trying to get my head around what is valid CNF and how distribution works, I am not even sure if the examples I have tried to convert are correct for one, but I am also unsure of the rule ...
- 81
1
vote
1
answer
895
views
Boolean logic: why is the "opposite" of and equal to or?
In boolean logic, why is the "opposite" of AND (&) equal to OR (|)?
For example, why would ...
1
vote
2
answers
118
views
Propositional Logic: Entailment
Given the sentences, S1, S2, if S1 |= S2 then all models that satisfy S1 also satisfy S2, how is the following statement correct?
A ∧ ¬A |= B
How can something and ...
- 81