Questions tagged [propositional-logic]

The tag has no usage guidance.

Filter by
Sorted by
Tagged with
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 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,...
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: ...
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(\...
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 ...
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) ...
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 ...
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?
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. ...
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 ...
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 ...
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 )\...
  • 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 ...
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 ...
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