Questions tagged [logic]

Question 1

I'm trying to do variable elimination by resolution in CNF SAT formulas. According to Wikipedia and other sources, the resolution rule states that $$ \dfrac{(p \lor a) \land (\neg p \lor b)}{(a \lor b)...

Question 2

I'm trying to understand how to interpret the turnstile notation Γ ⊢ A when it appears in natural deduction systems, and I'm confused about the relationship between natural deduction and sequent ...

Question 3

The following encodes the existential quantifier in λC, in a context where $S:*, \; P,Q : S \to *$. $$\Pi \alpha:*. (\Pi x:S.(Px \to \alpha)) \to \alpha$$ I can work through the mechanics showing ...

Question 4

I wanted to develop a tree-format natural deduction of the following tautology. $$ \exists_{x \in S}(P(x)) \quad \implies \quad ( \forall_{y \in S}(P(y) \implies Q(y)) \implies \exists_{z \in S}(Q(z))...

Question 5

I'm really struggling with this exercise 7.8(b) from Type Theory and Formal Proof. Give λC-derivations verifying the following tautologies of constructive logic (hint: use Exercise 7.7 and Section 7....

Question 6

I am trying to understand the complexity of a problem that involves solving some $\mathsf{PSPACE}$-complete problem exponentially many times. Namely, one can imagine $\Xi=\{\phi_1,\ldots,\phi_n\}$ to ...

Question 7

Exercise 7.6(c) from Type Theory and Formal Proof (Nederpelt) asks us to derive in λC an inhabitant of a type that corresponds to the following logical statement: $$\neg(A \land B) \implies (A \...

Question 8

In my Theory of Computability class, our final project is to write a Turing Machine in JFLAP. My project is to write one able to validade a logic formula in postfix notation. So, for example: input: ...

Question 9

I am currently trying to understand the IC3/PDR algorithm. My intuitive understanding is that in each iteration, IC3 tries to find a counterexample $c$ (which is a single, concrete state) such that $c ...

Question 10

I'm following this online guide to quantifier inference rules for natural deduction [pdf]. Question: I need help as I don't understand two of the rules, $\forall$-intro and $\exists$-elim. I discuss ...

Question 11

I reading about the Law of the Excluded Middle, that in Classical Logic the following holds for any proposition $P$ $$P \lor \neg P$$ Question: Is that an "OR" or is it an "XOR"? ...

Question 12

I'm worried that my question might be ill-posed, but I've tried to formulate it as precisely as possible. As a computational model, lambda calculus has numerous alternatives, including Turing machines....

Question 13

Exercise 6.5 of Type Theory and Formal Proof (Nederpelt) asks us to interpret logically the following judgement: $$ S : * \quad \vdash \quad \lambda Q : S \to S \to *. \lambda x : S. Qxx \quad : \...

Question 14

I'm continuing to work through Chapter 5 of Type Theory and Formal Proof (Nederpelt). Doing exercise 5.10 I've run into a wall. I know there is a correspondence between λP types and logical ...

Question 15

Exercise 5.6 in Type Theory and Formal Proof asks us to first develop a natural deduction proof of the following logical statement (before doing a λP derivation). $$ (A \implies (A \implies B)) \...

Stack Exchange Network

Questions tagged [logic]

Proof of variable elimination via resolution

Understanding the ⊢ notation and context in Natural Deduction vs Sequent Calculus

How to "read" the λC encoding of the existential quantifier $\Pi \alpha:*. (\Pi x:S.(Px \to \alpha)) \to \alpha$

scope of "constant symbol" in tree-format natural deduction

finding an inhabitant in λC to show tautology $¬(A∨B) ⇒(¬A∧¬B)$

Repeating a PSPACE problem exponentially many times

finding inhabitant of type corresponding to $\neg(A \land B) \implies (A \implies \neg B)$

Turing Machine for postfix Logic Formula

IC3/PDR: Why is $\neg s$ included in the relative induction query?

help understanding quantifier rules for natural deduction

Is the Law of the Excluded Middle "Or" or "Xor"?

Why does lambda calculus have clear semantics, easy comprehensibility, and serve as a foundation for proof languages?

logical interpretation of λC type $(S \to S \to ) \to S \to $

Logical proposition corresponding to the λP type $\Pi x:S.*$?

convention for natural deduction proofs when lines are not used

Hot Network Questions