Questions tagged [natural-deduction]
The natural-deduction tag has no usage guidance.
5
questions
1
vote
0
answers
23
views
Discharging an assumption in Isar
In Isar, one can make an assumption and then use it as a premise for an implication goal later.
...
- 267
0
votes
1
answer
85
views
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 ...
- 23
1
vote
1
answer
60
views
2
votes
1
answer
220
views
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
...
- 123
1
vote
1
answer
110
views
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 ...
