Questions tagged [propositional-logic]

The tag has no usage guidance.

Filter by
Sorted by
Tagged with
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
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 ...
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
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 ...
3
votes
3answers
792 views

Does exist any horn formula that is equisatisfiable to the clause that is disjunction of two literals? Does also exist equivalent?

I just and simply want to know if whether or not exist any horn formula that is equisatisfiable to $(p\lor q)$. I would also be interested to know if there also exists equivalent.
0
votes
1answer
214 views

How to construct an NFA Ai for the given Regular property P1 and P2?

Let AP = {a; b; c}. Consider the following regular safety properties: (a) P1: If a becomes valid, afterwards b stays valid ad infinitum or until c holds. (b) P2: Between two neighbouring occurrences ...
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 $\...
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 ...
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
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
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 ...
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 ...
7
votes
4answers
6k views

Boolean algebraic expression vs Propositional logic expression

There is a lot of similarity between Propositional logic and Boolean algebraic expressions. Similar aspects : 1) Both has variables of two states. 2) Operations of Boolean algebra and ...
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 ...
1
vote
2answers
374 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 ...
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 ...
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 (...
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 ...
-2
votes
2answers
103 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
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
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 ...
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
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 ...
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
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 )\...
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 ...
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 ...
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 ...