Questions tagged [propositional-logic]

The tag has no usage guidance.

Filter by
Sorted by
Tagged with
0
votes
1answer
10 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
16 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
24 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
22 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
28 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
35 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
52 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
35 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
2answers
46 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
51 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
84 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
49 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. ...
2
votes
1answer
91 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 ...
-1
votes
3answers
93 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
38 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 ...
0
votes
0answers
15 views

Satisfaction of CTL

I'm trying to compute Sat(Φ), but I can't seem to figure out this question, what i understood is that I first need to solve Sat(req U -busy), but it doesn't make sense, how can it be that req is true ...
1
vote
0answers
21 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
42 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
66 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
0answers
27 views

About the complexity of deciding if the closed world assumption for renamable Horn CNF is consistent

Let $T$ be a theory that only contains renamable horn formulas. What is the complexity of deciding if the closed world assumption $CWA(T)$ is consistent? The closed world assumption is defined as ...
0
votes
1answer
53 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
37 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
76 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
47 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
137 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
15 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
51 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
44 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
40 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
64 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
67 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
46 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
97 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 ...
0
votes
2answers
36 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
36 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
42 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
41 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 ..." ...
-2
votes
2answers
83 views

How to correctly negate a predicate bounded by some quantifiers?

this is a problem which was asked in GATE CS 2010. This is question statement: Q: Suppose the predicate F(x, y, t) is used to represent the statement that person x can fool person y at time t. which ...
0
votes
0answers
40 views

How to write negation of an 'AND' statement in logic

Suppose the given proposition is: "Zach blocks emails and texts from Jennifer" Where, P implies "Zach blocks emails from Jennifer". Q implies "Zach blocks texts from Jennifer". So it's P AND Q in ...
1
vote
2answers
211 views

The optimized numbers of variables and clauses to encode a graph coloring problem in CNF

Problem Statement Given a finite graph $G = \langle V, E\rangle$, consisting of vertice set $V$ and edge set $E$, and a finite set of colors $C$, a problem instance of graph coloring is to assign ...
2
votes
1answer
50 views

Non-Boolean SAT

I was wondering about the complexity of SAT tests with variables $x_i = 0 \lor 1 \lor 2 \dots \lor n$, with clauses being of the form $x_i = a \implies x_j \neq b$. When $n=2$, we have 2SAT, which has ...
0
votes
2answers
66 views

prove that {$↔,⊕$} is incomplete set?

How do i prove that Is {$↔,⊕$} not a complete set ? I have no clue how to prove it .
3
votes
1answer
112 views

Are these 2 equivalent?

Is ∀x∀y∀z[φ(x,y)∧p(y,z)->p(x,z)] equivalent to ∀x∀y∀z[φ(x,y)∧p(x,z)->p(y,z)] ? The only thing I can think of is that this question can be answered if we show that ...
0
votes
2answers
129 views

Does the naive conversion of a Boolean Formula to CNF have a polynomial or exponential complexity?

I am reading the naive conversion to CNF, this procedure is explaining in this book book, but I have not found a conplexity analysis of this algorithm: elimination of equivalence Elimination of ...
0
votes
0answers
76 views

What are necessity and sufficiency?

I was reading deadlock topic from Operating Systems book by Stallings. It states four pre requisites for deadlock: Mutual exclusion No preemption Hold and wait Circular wait It then have following ...
1
vote
1answer
100 views

Context-free grammar for tautologies in one variable

Construct a context-free grammar for the set of tautologies in $p$ - that is, the set of formulae in $\{p, \text{true}, \text{false}, \land, \lor, \lnot, (, )\}$ which evaluate to $\text{true}$ for ...
1
vote
2answers
118 views

Are $\mathsf{\#P}$ problems harder than $\mathsf{NP}$ problems

I have a method to solve the $\mathsf{\#P}$ version of 3SAT in a way that seemingly reduces it to an $\mathsf{NP}$ problem. - I don't have a formal understanding of these terms so I will just show an ...
2
votes
1answer
77 views

3-CNF to “independent form”

Is it possible to convert all logical formulae into a form such that each variable ends up in exactly 1 "factor" of the and operation? ($\wedge$). Any combination of operations is allowed, though the ...