Questions tagged [propositional-logic]
The propositional-logic tag has no usage guidance.
207
questions
-1
votes
0
answers
24
views
Hoare Logic with how to find post condition
Consider the following program snippet: {a>0∧b>0}
as a precondition. Which of the following formulas is a postcondition for this program?
...
0
votes
1
answer
47
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
37
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
18
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
56
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
976
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
4
votes
1
answer
216
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 ...
- 1
1
vote
1
answer
133
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 ...
- 542
2
votes
2
answers
414
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
37
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
23
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
60
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
0
votes
1
answer
45
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 (\...
- 935
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
38
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 ...
- 935
1
vote
1
answer
40
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$ ...
- 935
0
votes
2
answers
119
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
68
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
138
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
48
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
163
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
210
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,141
1
vote
1
answer
154
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
32
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
52
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 \...
1
vote
1
answer
86
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 ...
- 11
1
vote
1
answer
80
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 ...
0
votes
0
answers
269
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
88
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
80
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
74
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
200
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
91
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
99
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
128
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
161
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
49
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
118
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
644
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
60
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
90
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
103
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
563
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
784
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
112
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
0
votes
1
answer
95
views
In propositional logic how is the negation equivalent?
I am unable to understand how the negation of a sentence into CNF actually makes sense, hopefully somebody can explain it to me in understandable terms!
Given the sentence: If the battery is charged (...
- 81