Questions tagged [natural-deduction]

The tag has no usage guidance.

Filter by
Sorted by
Tagged with
2 votes
1 answer

Natural deduction with coq assistant prover

I want to mimic natural deduction proofs in coq ; for instance the proof I made for "A /\ B -> B /\ A" is for now ...
Netchaiev's user avatar
  • 123
1 vote
1 answer

How to write a low-level proof in Isar?

I would like to formalize ...
Gergely's user avatar
  • 299
1 vote
1 answer

Natural deduction vs simply typed lambda calculus

In ND , I have propositions as their own things, but in simply typed lambda calculus, I have propositions associated with proof. The question I want to ask is, how do these two different way of ...
tryst with freedom's user avatar
1 vote
0 answers

Discharging an assumption in Isar

In Isar, one can make an assumption and then use it as a premise for an implication goal later. ...
Gergely's user avatar
  • 299
0 votes
1 answer

Natural deduction in Coq

I am trying to verify the proofs by natural deduction from Ryan and Huth based on the information in Natural deduction with coq proof assistant. Here is Example 1.13 and its proof. Step 4 is ...
Moti's user avatar
  • 23