Questions tagged [propositional-logic]

The tag has no usage guidance.

Filter by
Sorted by
Tagged with
-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?
user avatar
-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 ...
user avatar
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 ...
user avatar
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 ...
user avatar
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 ...
user avatar
  • 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 ...
user avatar
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 $\...
user avatar
  • 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 ...
user avatar
  • 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(\...
user avatar
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 ...
user avatar
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) ...
user avatar
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 ...
user avatar
  • 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 ...
user avatar
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 ...
user avatar
  • 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 ...
user avatar
  • 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 ...
user avatar
  • 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?
user avatar
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} ...
user avatar
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 ...
user avatar
  • 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 ...
user avatar
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 ...
user avatar
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 ...
user avatar
  • 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 ...
user avatar
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 ...
user avatar
  • 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 (...
user avatar
  • 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 ...
user avatar
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.
user avatar
  • 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. ...
user avatar
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 ...
user avatar
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 ...
user avatar
  • 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 ...
user avatar
  • 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_{...
user avatar
  • 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 ...
user avatar
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 ...
user avatar
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 ...
user avatar
  • 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 )\...
user avatar
  • 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, $\...
user avatar
  • 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 ...
user avatar
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....
user avatar
  • 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 ...
user avatar
  • 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 ...
user avatar
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 ...
user avatar
  • 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 ...
user avatar
  • 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 ...
user avatar
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). ...
user avatar
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 ...
user avatar
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]$...
user avatar
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 ...
user avatar
-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 ...
user avatar
  • 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....
user avatar
  • 51