Questions tagged [propositional-logic]

The tag has no usage guidance.

Filter by
Sorted by
Tagged with
1 vote
1 answer
64 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 ...
1 vote
1 answer
168 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 ...
3 votes
1 answer
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 ...
1 vote
1 answer
74 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 ...
2 votes
4 answers
3k views

Resolution and what it means to derive the empty set

When using resolution, if the empty set {Ø} is derived from a formula like {¬x,¬y} {x,y}, does that mean the formula is unsatisfiable? If this is the case, why is ...
2 votes
2 answers
393 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 ...
1 vote
0 answers
30 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 ...
1 vote
0 answers
21 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 ...
0 votes
1 answer
35 views

How big is a formula equivalent to a wff over $n$ variables with $2^n$ subformulas?

Definitions: Let $n \in \mathbb{N}$. If $\alpha$ and $\beta$ are propositional formulas, then we'll call $\alpha$ and $\beta$ independent if neither implies the other, or more formally, if $\lnot (\...
-1 votes
2 answers
87 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 ...
0 votes
2 answers
51 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 ...
2 votes
0 answers
23 views

Stålmarck's method, can triplets be dropped once they triggered equivalences

In Sheeran, Mary, and Gunnar Stålmarck: A tutorial on Stålmarck’s proof procedure for propositional logic there is an example application of the method to...
0 votes
0 answers
36 views

Growth of a set of propositional formulas under partial evaluation

Definitions: Let $n \in \mathbb{N}, n \geq 1$. We write $|\alpha|$ to denote the length in characters of an expression $\alpha$ in propositional logic. We define partial evaluation in the normal way ...
1 vote
1 answer
39 views

Complexity of a Set of Formulas

Notation: We write $|\alpha|$ to denote the length in characters of an expression $\alpha$ in propositional logic. Consider an expression $\alpha_n$ in disjunctive normal form built from $2n$ ...
0 votes
2 answers
177 views

a program discovering himself how to solve propositional calculus

it is well-known that propositional logic problems such as $$ (p\leftrightarrow q) \lor r \quad\overset{?}{\vdash}\quad (((p\lor q)\to(p\land q)) \land \lnot r)\lor r$$ can be simply solved by ...
4 votes
1 answer
465 views

A Quine–McCluskey variant for conjunctive normal form?

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?...
0 votes
1 answer
128 views

Is "Bitwise Complement Operator" (~ tilde) distributive?

To be more precise, Is ~(a+b) = ~a + ~b? Here, "~" bitwise NOT operator. I ran into this question while thinking about ...
0 votes
0 answers
37 views

What are the applications of Belief Revision?

In my Computer Science graduation, I came across this concept of Belief Revision, which focus on knowledge representation and the possible operations that can be done with the facts that a "...
0 votes
2 answers
54 views

Is T V F a tautology?

(Consider $T=true$, $F=false$) I apologize for the simple question but I'm confused as to what is a tautology and what isn't and I haven't found a clear definition. I think that a tautology is a ...
-1 votes
4 answers
609 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 ...
2 votes
1 answer
38 views

Sequent calculus and vs comma: $a \land b \implies ...$ vs $a, b \implies ...$

I was reading "Open Logic book", "Sequent Calculus". Given the fact that all antecedents must hold for at least one succedent to hold, I can't get rid off the impression that using ...
0 votes
1 answer
63 views

Is any 2-CNF has 2-DNF representation?

I was asked a question whether I could come up with a 2-CNF over several variables that has no 2-DNF representation. However I thought that any CNF can be converted to DNF through some manipulations e....
0 votes
0 answers
64 views

Proving that the polish notation has unique readability

I am familiar with the polish notation when it comes to algorithmically reading phrases, but I am having a hard time proving the following exercise: K is a function so that 1) $K(*)$ is an integer if ...
0 votes
1 answer
384 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 ...
1 vote
0 answers
48 views

Application of a formal definition of $max, min$ to evaluate an expression

For an Algorithms course we are studying propositional calculus. As an excercise we are given formal statements which we are to explain in natural language first and then evaluate with specific values....
0 votes
2 answers
180 views

My attempt at the "This statement is false" paradox

(I haven't read any literature on this paradox nor am I good at formal proofs, so this is just my intuitive thoughts on the paradox.) If we assume the statement "This statement is false" as ...
1 vote
1 answer
74 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 ...
5 votes
3 answers
4k views

Find hamilton cycle in a directed graph reduced to sat problem

I need to find a Hamiltonian cycle in a directed graph using propositional logic, and to solve it by sat solver. So after I couldn't find a working solution, I found a paper that describes how to ...
2 votes
3 answers
1k views

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

I just want to know whether there exists a horn formula that is equisatisfiable to $(p\lor q)$. I would also be interested to learn if there exists an equivalent as well.
0 votes
1 answer
106 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
1 answer
120 views

Proof that propositional resolution is refutation complete

I am studying theoretical computer science and I am in the part about resolution in propositional calculus. I was reading a theorem (and its proof) that propositional resolution is refutation complete,...
0 votes
1 answer
30 views

How to get the formal model using propositional logic

Input There are three chairs (1,2,3) in the same row. We need to find a seat for three guests (a,b,c). Constraints The first guest does not want to be seated next to the third one (neither left nor ...
0 votes
2 answers
50 views

Logical equivalence priority

I have the logical formula $$ A \Leftrightarrow B \Leftrightarrow C $$ In order to make the truth table I'm not sure wheither I should interpret it as $A \Leftrightarrow B \Leftrightarrow C$ or $A \...
0 votes
0 answers
213 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 ...
3 votes
1 answer
76 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
1 answer
68 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
1 answer
173 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
1 answer
171 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 $\...
0 votes
1 answer
82 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
2 answers
97 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
2 answers
116 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
3 answers
1k 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
1 answer
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 ...
2 votes
2 answers
115 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
1 answer
132 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 ...
4 votes
1 answer
47 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
4 answers
9k 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 ...
2 votes
1 answer
452 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
0 answers
50 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
1 answer
65 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 ...

1
2 3 4 5