# Questions tagged [propositional-logic]

The tag has no usage guidance.

207 questions
Filter by
Sorted by
Tagged with
24 views

### Hoare Logic with how to find post condition

Consider the following program snippet: {a>0∧b>0} as a precondition. Which of the following formulas is a postcondition for this program? ...
47 views

### How would I prove implications of this structure?

Consider the following to prove: $(A \implies B) \implies (C \implies D)$ Could this be proved by assuming A then proving B, then using A and B to prove C, then using A, B and C to prove D? or would ...
• 173
37 views

### Satisfiability of a boolean formula with two occurrences of each variable with a special ordering

I am interested in the complexity of a special case of the boolean satisfiability problem: We are given a boolean formula, consisting only of the logical operators $\land$ and $\lor$ (that can be ...
• 161
18 views

### Finding a common variable value among all SAT solutions

Let $F$ be a boolean formula on $n$ variables $x_1, \cdots, x_n$. $\textbf{SAT}(F)$ asks whether there exists an assignment of truth values to variables under which $F$ is true. I'm curious about ...
56 views

### Why can't we say that P=NP if we have an infinite text file with solution for every possible SAT combination?

I believe that I have a misunderstanding in the P=NP problem while I was thinking of how can it be proved in a non-constructive manner. We know that we can build an infinitely large text file with ...
976 views

### Does Either...Or means Exclusive Or or Inclusive Or?

Let's take a compound propositions Either it is below freezing or it is snowing. Now if, $p$: it is below freezing $q$: it is snowing Question Link: https://gateoverflow.in/42720/kenneth-rosen-...
• 208
216 views

### Tseitin formula on 2-connected graph

How can we prove that for $\\\\$ every $\\\\$ 2-connected graph G with an odd number of vertices, the unsatisfiable Tseitin formula for it is minimally unsatisfiable, that is, if we remove even a ...
1 vote
133 views

### Resolution on weakening rule by derived clause

How to prove that every clause that is implied by the input formula (learned or not) can be derived using resolution with weakening rule: $\frac{C} {C \vee D}$ (A clause $C$ is implied by $F$ if for ...
• 542
414 views

### I've heard that it isn't possible to encode product types and sum types in a simply typed lambda calculus, but it seems for me that it's false

Of course, it isn't possible to construct them directly since we hasn't these type constructors, but only function constructor (arrow). But suppose there are 2 types $A$ and $B$, from which we need to ...
• 109
1 vote
37 views

### What logical system does hindley-milner correspond to, according to the curry howard correspondence?

If I understand CHC correctly, simply typed lambda calculus corresponds to propositional logic. As HM allows polymorphic definitions by let-expressions, my guess is that it would correspond to a ...
• 36
23 views

### SAT for clauses of the form "At most m out of n are false"

Recall some terminology: Let $\mathsf P$ be a finite set of propositional atoms, and let $\Phi$ be a proposition over $P$ that is generated from $\top$, $\bot$, $\neg$, $\wedge$, and $\vee$. Then: A ...
• 171
60 views

### Is there a model for the given logical formula, and if not, why?

I'm trying to determine whether there exists a model for the following logical formula: $(p_1 \to (p_2 \lor p_3)) \land(p_2 \to \neg p_3) \land ((p_1 \lor p_3) \to \neg p_2)$. Here's my understanding ...
45 views

1 vote
86 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 ...
• 11
1 vote
80 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 ...
269 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 ...
88 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 ...
80 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
74 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 ...
200 views

128 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 ...
2k 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) ...
• 133
1 vote
161 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
49 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
100 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
118 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
86 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
644 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?
60 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
90 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
27 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 ...
103 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 ...
563 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
784 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
112 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