Questions tagged [propositional-logic]
The propositional-logic tag has no usage guidance.
161
questions
0
votes
1answer
28 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
votes
0answers
19 views
Writing an equivalent to (p->q)/\r using only ∼ and ∨
Trying to write (p->q)/\r using only ∼ and ∨ but always getting stuck .
0
votes
1answer
34 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
43 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
74 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
82 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
32 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
14 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
20 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
31 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
50 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
25 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
44 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
34 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
72 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
40 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
93 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
47 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
40 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
37 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
44 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
43 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
45 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
56 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
35 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
36 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
36 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
..." ...
0
votes
1answer
51 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
1answer
124 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
44 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
60 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
99 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
57 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
78 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
111 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
75 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 ...
2
votes
1answer
65 views
Conjunctive normal form to simple elementary algebra
I'm curious to know the computational complexity class of each step in this method of converting a CNF formula into simple elementary algebra.
An example:
$$\phi=\left(x_1 \vee x_2 \right) \wedge \...
1
vote
1answer
99 views
Algorithm for automatic construction of natural deduction proofs
I was wondering if there exists any algorithm for automatic construction of nautral deduction proofs. I'm interested in propositional logic and first order logic.
If there is no algoritm, can you ...
2
votes
0answers
98 views
A Quine–McCluskey variant for conjunctive normal formal?
There is the Quine–McCluskey algorithm for finding a minimal expression of a boolean expression in dis-junctive normal form. Would applying DeMorgan's rule to the minimal DNF result in the minimal CNF?...
4
votes
3answers
114 views
Is it a tautology or not? According to my truth table its not
If $\bigr((q\leftrightarrow p)\leftrightarrow s\bigl)$ is a tautology and $p\rightarrow s$ is contingent, does it follow that $q\rightarrow s$ is contingent?
Since I can't show $\bigr((q\...
4
votes
0answers
45 views
Is there a correspondence of steps between DPLL and sequent-calculus?
Is there a correspondence between the steps in using DPLL to find out that a formula in propositional logic is unsatisfiable and using sequent calculus to prove that its negation is valid?
And given ...
2
votes
1answer
32 views
How do I determine if this argument is valid?
I'm studying propositional logic the section on "valid arguments".
A self-assessment question reads
"Show whether or not the following argument is valid"
$\frac{P}{C}$
I don't know what function ...
1
vote
1answer
27 views
Does “$\forall x\in L, \sigma(\neg x)=\neg \sigma(x)$” hold given that $\sigma(F)\equiv F$ for a CNF formula $F$ built on a set $L$ of literals?
Suppose we have a CNF formula $F$ built on the set of literals $L=\{x_1,\neg x_1,\cdots,x_n,\neg x_n\}$ where each variable is used in at least one clause of $F$. Consider a permutation $\sigma$ of $L$...
0
votes
2answers
63 views
Why we treat sentence letter $Q$ as conclusion in one form and premise in other?
Sorry for asking such a dumb question.
I am CS student and I am trying to understand the basic tenets of Logic. I am new to the subject and I am lost understanding Implication.
In formal logic, $(P\...
