Questions tagged [propositional-logic]

The tag has no usage guidance.

34 questions with no upvoted or accepted answers
Filter by
Sorted by
Tagged with
4 votes
0 answers
70 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 ...
Alex's user avatar
  • 263
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...
user3128's user avatar
2 votes
0 answers
64 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 ...
user109711's user avatar
2 votes
0 answers
140 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 ...
M. McIlree's user avatar
2 votes
0 answers
128 views

Why Modus ponens works with Horn clauses and Generalized Modus ponens requires definite clauses?

I am reading the Artificial Intelligence: A Modern Approach book and in the chapters about logic i noticed that in propositional logic the Modus ponens inference rule (used by the forward and backward ...
Marco Cadei's user avatar
2 votes
0 answers
68 views

What is the difference between the situation calculus and the propositional logic of context?

I have been reading a lot of papers by John McCarthy lately. As early as 1963, he developed the situation calculus, but then starting in 1987, he developed what came to be known as the propositional ...
robguinness's user avatar
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 ...
pgmcr's user avatar
  • 36
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 ...
Jim's user avatar
  • 111
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....
lafinur's user avatar
  • 181
1 vote
1 answer
75 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 ...
A. Boy's user avatar
  • 11
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 ...
Smiley's user avatar
  • 9
1 vote
0 answers
45 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_{...
MATH_LI's user avatar
  • 11
1 vote
0 answers
26 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). ...
johnrogeksu's user avatar
1 vote
0 answers
203 views

How to minimize large DNF formula into deeper but smaller formula?

I want to minimize DNF formula which has ~200k products combined into a sum. The depth of that formula is 2 - first level is the OR, and second level is AND for all conjunctions. I have tried using ...
Nikola Dim's user avatar
1 vote
0 answers
92 views

What is the definition of the property of Canonicity for a logic?

I'm trying to understand "A Systematic Approach to Canonicity in the Classical Sequent Calculus" by Kaustuv Chaudhuri, Stefan Hetzl, Dale Miller. The article discusses a property called "canonicity" ...
ttbo's user avatar
  • 113
1 vote
0 answers
102 views

Refutation of pigeonhole using resolution

I am trying to find a way to refute the pigeonhole formula using resolution. Lets assume that $x_{ij}$ is true if $i^{th}$ pigeon is in $j^{th}$ hole. Thus, with $n$ holes and $n+1$ pigeons, the ...
Sayan Pal's user avatar
  • 111
1 vote
0 answers
288 views

Propositional logic in an SMA* algorithm

I'm trying to implement an SMA* graph search algorithm that I found in a paper here(Rong Zhou, Eric A. Hansen: Memory-Bounded A* Graph Search. FLAIRS-02 Proceedings 203-209) and I would like to ...
moremilopls's user avatar
1 vote
0 answers
36 views

What does the structure ($S_t^x P$) in this Existantial Instantiation imply, Skolemization?

The sheet of equivalences given to us in class provides the two equivalences \begin{array}{|c|c|c|} \hline \text{Universal Instantiation} & \forall x ~ P(x) \implies {S_t}^x P & \exists y ~ \...
KDecker's user avatar
  • 343
1 vote
0 answers
126 views

Efficiently decidable logics

So propositional logic (PL) is efficiently (in P) decidable because I can convert formulas to an equisatisifiable CNF-formula, negate and convert (efficiently, by De Morgans laws) to DNF. I can then ...
Jake's user avatar
  • 3,800
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 (\...
ShyPerson's user avatar
  • 923
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 ...
ShyPerson's user avatar
  • 923
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 "...
Jonas's user avatar
  • 103
0 votes
0 answers
65 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 ...
Tita's user avatar
  • 225
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 ...
Farewell Stack Exchange's user avatar
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} ...
Redone123's user avatar
0 votes
0 answers
65 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. ...
მამუკა ჯიბლაძე's user avatar
0 votes
0 answers
304 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 ...
twinrix's user avatar
  • 13
0 votes
0 answers
79 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 ...
Utsav Prasad's user avatar
0 votes
0 answers
155 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 ...
RajS's user avatar
  • 1,647
0 votes
0 answers
144 views

Resolution with multiple variables

Resolution allows to generate new clauses for an existing set of clauses. In many cases, the rule is simple: ...
just.kidding's user avatar
0 votes
0 answers
153 views

Convert conjunctive normal form to equivalent boolean formula with only NOR gates

Let $\varphi$ be a boolean formula in 3-CNF form (conjunctive normal form with three literals at most per clause). I want to convert it to an equivalent boolean formula that uses only NOR gates with ...
Farewell Stack Exchange's user avatar
-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 ...
Thomas Iskandar's user avatar
-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 ...
Smiley's user avatar
  • 9
-1 votes
1 answer
28 views

C logical consequence of S iff S union {-C} UNSAT

I'm trying to do the following demonstration: (C and S are CNF) C is a logical consequence of S iff. S u {-C} UNSAT And I did the following: C is a logical consequence of S iff. S u {-C} UNSAT iff. ...
Norhther's user avatar
  • 117