Questions tagged [propositional-logic]
The propositional-logic tag has no usage guidance.
191
questions
0
votes
0
answers
39
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....
- 111
0
votes
1
answer
79
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
0
answers
8
views
State of the art construction of OBDDs
I have some Boolean functions represented by pretty big Boolean formulas and I need to build OBDDs from the formulas for further manipulation. How to do it is well known with textbook algorithms but I ...
- 448
0
votes
2
answers
122
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,101
1
vote
1
answer
39
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,...
- 290
0
votes
0
answers
23
views
Hoare Logic - Interpreting identity
I'm having some issues on understanding the following identity:
{ P } S { Q } ≡ [P ⇒ wp.S.Q]
Does this means that if I have something like:
...
- 1
0
votes
1
answer
28
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
38
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
52
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 ...
- 1
1
vote
1
answer
61
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
118
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 ...
0
votes
2
answers
73
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
57
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
41
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
86
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
47
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
...
- 247
-1
votes
2
answers
94
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
100
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 ...
- 3
2
votes
3
answers
763
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
90
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
43
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
97
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
3
votes
2
answers
111
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
2
votes
1
answer
80
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
1
vote
1
answer
209
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?
- 35
0
votes
0
answers
38
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
44
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
26
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 ...
1
vote
1
answer
60
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
260
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
144
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
64
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
82
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
0
votes
1
answer
102
views
Is Conjunctive Normal Form or not?
I have one formula that I do not understand why it is CNF and one that is not CNF, namely.
p && !q (NOT NCF)
and
!!p(CNF).
According to the exercise where I found these examples, 1 is not ...
1
vote
1
answer
562
views
Is it generally possible to convert CNF to Horn clauses?
My intuition is that it is not generally possible, but I cannot think of a proof.
- 369
0
votes
0
answers
61
views
When are existential quantifiers in the intuitionistic propositional calculus eliminable and when not
I am so ignorant I don't even know where should I ask this - on FOM? On mathoverflow? On cstheory? So please consider as sort of a meta-question readdressing me in case you think this is a wrong site. ...
- 101
3
votes
1
answer
146
views
What is the purpose of learning propositional logic
I am in an AI class where we have extensively learned about propositional logic.
I am wondering what the point of learning this is? Are there any uses for propositional logic? Beyond basic logic gates ...
- 135
0
votes
4
answers
513
views
Prove (p → ¬q) is equivalent to ¬(p ∧ q)
I need to prove the above sequent using natural deduction. I did the first half already i.e. I proved $(p\rightarrow\neg q)\rightarrow \neg (p \wedge q)$, but I'm stuck on where to start for the ...
- 11
1
vote
1
answer
145
views
Proving the validity of a sequent using Modus Tollens
Problem: Prove $p \rightarrow (q \vee r), \neg q, \neg r \vdash \neg p$ using Modus Tollens.
I need to prove the validity of the above sequent by using natural deduction. Initially, I didn't read the ...
- 11
1
vote
0
answers
34
views
Computational complexity in Boolean network
An Boolean control networks can be expressed as
\begin{equation}
\label{ControlBN}
\left\{\begin{array}{l}{x_{1}(t+1)=f_{1}\left(x_{1}(t), \cdots, x_{n}(t), u_{1}(t), \cdots, u_{m}(t)\right),} \\ {x_{...
- 11
0
votes
0
answers
206
views
Simplify logical expression represented as binary tree
I implemented logical expressions using a binary tree in C++. Now I want to be able to simplify such an expression using rules like e.g.
but have issues with the commutativity. Assuming the ...
- 3
0
votes
1
answer
133
views
What does it mean to "show algebraically" in propositional logic?
The biconditional operator $\iff$ of Propositional Logic can be defined by the identity
$p \iff q \equiv (\lnot p \lor q) \land (\lnot q \lor p) \quad (1.1)$
Use the identity $(1.1)$ and identities ...
0
votes
1
answer
81
views
How are prime implicates of HORN-Formulas defined?
I'm confused about the definition of prime implicates in Horn formulas.
For example in the paper of Kira 2012 on page 109 it is stated:
Now in the paper of Boros 2010 on page 82 the following ...
- 155
-1
votes
1
answer
71
views
Equivalence of Horn formulas tractable?
Assume I have two Horn formulas $\phi_1, \phi_2$. Horn formulas are CNF formulas so that each clause has at most one unnegated literal. For example:
$x_1 \wedge (\neg x_1 \vee \neg x_2 \vee x_3 )\...
D.W.♦
- 150k
2
votes
2
answers
117
views
Equivalence of Krom formulas tractable?
Assume I have two Krom formulas $\psi_1, \psi_2$. Krom formulas are propositional formulas in CNF that have 2 literals in every clause. Each literal can be negated or unnegated. In other words, $\...
- 155
0
votes
1
answer
54
views
Consistent theory based on L and not(A->A) is a theorem
I am working on this problem in which I have a theory $T$ based on language $\mathcal{L}$ and the only information we have is that T is consistent and $\vdash \lnot(A \rightarrow A)$. Given this ...
- 109
1
vote
1
answer
477
views
Is Monotone 3-SAT with exactly 3 distinct variables untractable?
I have given the following SAT variation:
Given a formula F in CNF where each clause C has exactly 3 distinct literals and for each C in F either all literals are positive or all literals are negated....
- 155
2
votes
1
answer
33
views
Circuits and formulas for Clique
Is it correct to say that the Clique Problem is in $P$ iff there exists a family of Boolean circuits $C$ to decide Clique whose sizes are bounded by a polynomial? And based on this question, does that ...
- 820
2
votes
0
answers
60
views
An optimization version of 2QBF: is it $\mathsf{NP}^{\mathsf{NP}}$-hard?
I am studying the computational complexity of the following decision problem related to 2QBF:
Input: a 3-CNF formula $\varphi$ over $X \cup Y$, where $X$, $Y$ are disjoint sets of propositional ...
- 95
3
votes
1
answer
85
views
"State of the art" algorithms deciding entailment of propositional formulas?
I fail to find much about how to efficiently calculate whether a propositional formula entails another.
Considering the following two points...
We can check, for each truth assignment which makes the ...
- 213