Questions tagged [propositional-logic]
The propositional-logic tag has no usage guidance.
183
questions
-1
votes
0
answers
18
views
Modal logic S4 system
How to prove in S4 system modal logic that ◇□◇x->◇x? Probably i only need to show that ◇□x->x
Any help will be great?
- 1
-4
votes
0
answers
72
views
2-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 2-Satisfiability is NP Complete first it must be showed ...
0
votes
0
answers
62
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
64
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
43
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
27
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
40
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 $\...
- 103
0
votes
1
answer
38
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
91
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
77
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
547
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
76
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
3
votes
1
answer
39
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 ...
- 33
1
vote
1
answer
93
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 ...
- 99
2
votes
2
answers
108
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 ...
- 99
2
votes
1
answer
76
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 ...
- 99
1
vote
1
answer
78
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
30
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
29
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
24
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
47
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
142
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 ...
- 83
1
vote
1
answer
71
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
48
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 ...
- 83
0
votes
1
answer
69
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 (...
- 83
0
votes
1
answer
85
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
384
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.
- 359
0
votes
0
answers
55
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
121
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
3
answers
342
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
108
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
27
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
170
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
110
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
72
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
60
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.♦
- 141k
2
votes
2
answers
105
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
53
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
322
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
28
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 ...
- 870
2
votes
0
answers
58
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
66
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
2
votes
1
answer
70
views
Unification Algorithm without Occur Check
I have been reading about Unification algorithm here https://en.wikipedia.org/wiki/Unification_(computer_science)#A_unification_algorithm
. And I wonder about the importance of occur check.
I know ...
- 23
2
votes
1
answer
209
views
Convert propositional logic formulas to mathematical constraints
Brief introduction
In all boolean (or more generally mixed-integer) linear programs, constraints are represented as a matrix $A$, a support vector $b$ and is computed by $A^T x \leq b$, where $x$ is ...
- 129
1
vote
0
answers
26
views
Correctness of Simple Programs
For a homework assignment I am asked to provide claim sequences to verify that the given conditional does indeed satisfy its specification (to compute in r the absolute value of x).
...
- 11
2
votes
0
answers
115
views
Large Conjunctive Normal Form Examples
I'm currently learning about conjunctive normal form in a course on logic for Computer Science. I was reading the Wikipedia entry on the subject and encountered this:
Typical problems in this case ...
- 131
2
votes
1
answer
54
views
Programming in Propositional Logic article notation question
I was reading this article about propositional logic and transforming problems to SAT. The author often uses the following notation (taken from Dominating set section):
I don't understand what $[v,i]$...
3
votes
1
answer
221
views
Definition of 2-CNF (a.k.a Krom) formula
In my lecturer's notes, the following definition for a 2-CNF wff is given:
A 2-CNF formula, or Krom formula is a CNF formula F such that every clause has at most two literals.
However, there is ...
-1
votes
2
answers
59
views
What if P implies Q is false when both P and Q are false?
This is actually a problem that our professor gave us, and I'm clueless of how to answer this. I browsed through various sources, but none were helpful regarding this question.
The question is,
In ...
- 131
0
votes
1
answer
28
views
Embedded arithmetic set expressions
In set builder notation, we can represent the set: $$\{ 2, 7\}$$ as: $$\{ x | x=2 \vee x=7 \}$$.
Therefore, the PA arithmetic predicate: $$φ(x) := x=2 \vee x=7$$ is capable of representing this set....
- 51