Questions tagged [natural-deduction]

The tag has no usage guidance.

Filter by
Sorted by
Tagged with
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. ...
0 votes
1 answer
108 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 ...
1 vote
1 answer
64 views

How to write a low-level proof in Isar?

I would like to formalize ...
2 votes
1 answer
232 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 ...
1 vote
1 answer
117 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 ...