Questions tagged [propositional-logic]
The propositional-logic tag has no usage guidance.
180
questions
3
votes
1answer
37 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 ...
-1
votes
1answer
19 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
1answer
36 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 $\...
0
votes
1answer
30 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
...
-1
votes
2answers
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(\...
0
votes
2answers
70 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 ...
2
votes
3answers
465 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) ...
1
vote
1answer
71 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 ...
3
votes
1answer
36 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 ...
1
vote
1answer
89 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 ...
2
votes
2answers
105 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 ...
2
votes
1answer
71 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 ...
0
votes
0answers
21 views
Software for proving tautology with steps
I'm looking for a software which can prove a tautology using logical equivalences.
It should be able to show each step. So you can follow the chain of reasoning.
Here is an example:
\begin{align}
(p\...
1
vote
1answer
44 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?
0
votes
0answers
24 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
1answer
25 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 ...
0
votes
1answer
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
1answer
35 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
1answer
78 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 ...
1
vote
1answer
68 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
2answers
40 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 ...
0
votes
1answer
54 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 (...
0
votes
1answer
78 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
1answer
248 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.
0
votes
0answers
54 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. ...
3
votes
1answer
111 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 ...
0
votes
3answers
256 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 ...
1
vote
1answer
84 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 ...
1
vote
0answers
24 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_{...
0
votes
0answers
120 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 ...
0
votes
1answer
101 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
1answer
63 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 ...
0
votes
1answer
47 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 )\...
2
votes
2answers
93 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, $\...
0
votes
1answer
48 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 ...
1
vote
1answer
229 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....
2
votes
1answer
23 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 ...
2
votes
0answers
56 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 ...
3
votes
1answer
51 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 ...
2
votes
1answer
55 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 ...
2
votes
1answer
159 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 ...
1
vote
0answers
24 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).
...
2
votes
0answers
99 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 ...
2
votes
1answer
50 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]$...
2
votes
1answer
178 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
2answers
57 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 ...
0
votes
1answer
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....
0
votes
1answer
42 views
Representing a sentence using propositional logic
I am confused regarding a propositional logic representation of a sentence.
Please note that this sentence is not realistic:
"A person who is male (M) is smart (S) if he is tall (T), but otherwise ...
1
vote
1answer
43 views
Complexity of negation cancellation
Consider propositional logic over the connectives $\land$, $\lor$, and $\lnot$. Notation: $| \alpha |$ is the length of formula $\alpha$.
We are given a formula $\phi$. Cancel all cancellable ...
2
votes
1answer
71 views
Significance of quantifier ordering in quantified boolean formulas (kQBF vs. QBF)
I am studying solvers of quantified boolean formulas (QBF) as a generalization of SAT solving. The standard DIMACS format of SAT specification is extended to QDIMACS, which adds "a ..." and "e
..." ...
