Well you have wrong names for your rules:
% (C=>X->Y) --> [(C,X=>Y)]
reduction(impI, (C=>X->Y), [[X|C]=>Y], []).
% (C,X->Y=>Z) --> [(C=>X),(C,Y=>Z)]
reduction(impE, (C0=>Z), [C=>X,[Y|C]=>Z], [H]) :-
use_hyp((_->_), C0, (X->Y), C, H).
They should be called impR and impL.
They are both introduction rules and not from
natural deduction but from sequent calculus.
**You might want to check Jens
Ottens leanSeq for correct names**
They are usually displayed with R and L,
for Right introduction and Left introduction,
backward search formulation with large context C:
C, X ⊢ Y
-------------- (R⊃)
C ⊢ X ⊃ Y
C ⊢ X C, Y ⊢ Z
--------------------- (L⊃)
C, X ⊃ Y ⊢ Z
In sequent calculus there are only Right
introduction and Left introduction for
the analytic part of the calculus that works
analytically on the different connectives.
On the the other hand natural deduction has
Introducton I rules and Elimination E rules,
and the calculus is non-analytic. The rules
would be totally different than what your code
uses and but wrongly labels with intro and elim:
C, X ⊢ Y
-------------- (I⊃)
C ⊢ X ⊃ Y
C ⊢ X C ⊢ X ⊃ Y
--------------------- (E⊃)
C ⊢ Y
The only shape agreement between natural deduction
and sequent calculus is the introduction rules
und right rules usually are the same inference rules,
i.e. we have (I⊃) = (R⊃). But the elimination rules
and left rules are usually differently shaped,
i.e. we have (E⊃) != (L⊃).
Julio Di Egidio schrieb:
On 21/12/2024 02:03, Mild Shock wrote:
Well you have to name it natural deduction
and not gentzen. It goes back to Stanisław Jaśkowski:
I prefer calling things by their name, you a spamming moron.
-Julio
--- SoupGate-Win32 v1.05
* Origin: fsxNet Usenet Gateway (21:1/5)